src/HOL/Lex/Auto.ML

--- a/src/HOL/Lex/Auto.ML	Sat Feb 28 15:41:17 1998 +0100
+++ b/src/HOL/Lex/Auto.ML	Sat Feb 28 15:41:50 1998 +0100
@@ -4,8 +4,6 @@
     Copyright   1995 TUM
 *)
 
-open Auto;
-
 goalw Auto.thy [nexts_def] "nexts A st [] = st";
 by (Simp_tac 1);
 qed"nexts_Nil";