Undo test change, update test output

Author: robsimmons

tests/lean/unknownTactic.lean

@@ -1,8 +1,6 @@
-theorem ex1 (x : Nat) : x = x → x = x :=
-  let q := by
-    intro
-    aexact (rfl)
-  q
+theorem ex1 (x : Nat) : x = x → x = x := by
+  intro
+  aexact (rfl)
 
 #print "---"
 

tests/lean/unknownTactic.lean.expected.out

@@ -1,15 +1,15 @@
-unknownTactic.lean:3:3: error: unknown tactic
-unknownTactic.lean:1:41-3:8: error: unsolved goals
+unknownTactic.lean:1:41-2:7: error: unsolved goals
 x : Nat
 a✝ : x = x
 ⊢ x = x
+unknownTactic.lean:3:2-3:8: error: unexpected identifier; expected command
 ---
-unknownTactic.lean:8:22: error: unknown tactic
-unknownTactic.lean:8:18-8:24: error: unsolved goals
+unknownTactic.lean:8:20-8:24: error: unexpected identifier; expected '{' or tactic
+unknownTactic.lean:8:18-8:20: error: unsolved goals
 x : Nat
 ⊢ x = x
 ---
-unknownTactic.lean:14:22: error: unknown tactic
-unknownTactic.lean:14:18-14:24: error: unsolved goals
+unknownTactic.lean:14:20-14:24: error: unexpected identifier; expected '{' or tactic
+unknownTactic.lean:14:18-14:20: error: unsolved goals
 x : Nat
 ⊢ x = x