diff -r fb28eaa07e01 -r 3ea049f7979d src/HOL/Lex/Scanner.ML
--- a/src/HOL/Lex/Scanner.ML	Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/Lex/Scanner.ML	Mon Jun 22 17:26:46 1998 +0200
@@ -4,7 +4,7 @@
     Copyright   1998 TUM
 *)
 
-goal thy
+Goal
  "DA.accepts (nae2da(rexp2nae r)) w = (w : lang r)";
 by(simp_tac (simpset() addsimps [NAe_DA_equiv,accepts_rexp2nae]) 1);
 qed "accepts_nae2da_rexp2nae";