src/HOL/Lex/AutoChopper1.thy

--- a/src/HOL/Lex/AutoChopper1.thy	Wed Mar 03 22:58:23 2004 +0100
+++ b/src/HOL/Lex/AutoChopper1.thy	Thu Mar 04 10:04:42 2004 +0100
@@ -17,7 +17,7 @@
 No proofs yet.
 *)
 
-AutoChopper1 = DA + Chopper +
+theory AutoChopper1 = DA + Chopper:
 
 consts
   acc :: "(('a,'s)da * 'a list * 's * 'a list list * 'a list * 'a list)