# HG changeset patch
# User nipkow
# Date 888676910 -3600
# Node ID f309259fa8287cf7aee840fa6542592ce23b32e1
# Parent  06f3c56dcba8d8b21f9c0abb047da0e138930811
Modified def.

diff -r 06f3c56dcba8 -r f309259fa828 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";
diff -r 06f3c56dcba8 -r f309259fa828 src/HOL/Lex/Auto.thy
--- a/src/HOL/Lex/Auto.thy	Sat Feb 28 15:41:17 1998 +0100
+++ b/src/HOL/Lex/Auto.thy	Sat Feb 28 15:41:50 1998 +0100
@@ -31,7 +31,7 @@
   "nexts(A) == foldl(next(A))"
 
   accepts :: ('a,'b) auto => 'a list => bool
-  "accepts A xs == fin A (nexts A (start A) xs)"
+  "accepts A == (%xs. fin A (nexts A (start A) xs))"
 
   acc_prefix :: ('a, 'b)auto => 'b => 'a list => bool
   "acc_prefix A st xs == ? us. us <= xs & us~=[] & fin A (nexts A st us)"