diff -r 0075a8d26a80 -r c7a869229091 src/HOL/Lex/AutoChopper.thy
--- a/src/HOL/Lex/AutoChopper.thy	Fri Aug 02 12:25:26 1996 +0200
+++ b/src/HOL/Lex/AutoChopper.thy	Thu Aug 08 11:34:29 1996 +0200
@@ -29,9 +29,9 @@
   auto_chopper_def "auto_chopper A xs == acc xs (start A) [] [] ([],xs) A"
 
 primrec acc List.list
-  acc_Nil  "acc [] st ys zs chopsr A =
+  "acc [] st ys zs chopsr A =
               (if ys=[] then chopsr else (ys#fst(chopsr),snd(chopsr)))" 
-  acc_Cons "acc(x#xs) st ys zs chopsr A =
+  "acc(x#xs) st ys zs chopsr A =
             (let s0 = start(A); nxt = next(A); fin = fin(A)
              in if fin(nxt st x)
                 then acc xs (nxt st x) (zs@[x]) (zs@[x])