diff -r cf1404c3f7bb -r a9fa93e1a86e src/HOL/Lex/AutoChopper.thy
--- a/src/HOL/Lex/AutoChopper.thy	Wed May 20 18:58:13 1998 +0200
+++ b/src/HOL/Lex/AutoChopper.thy	Mon May 25 12:55:01 1998 +0200
@@ -30,17 +30,17 @@
   acc :: "[('a,'s)da, 's, 'a list list*'a list, 'a list, 'a list, 'a list]
           => 'a list list * 'a list"
 primrec acc List.list
-  "acc A s r []     ys zs = (if ys=[] then r else (ys#fst(r),snd(r)))" 
-  "acc A s r (x#xs) ys zs =
+  "acc A s r ps []     zs = (if ps=[] then r else (ps#fst(r),snd(r)))" 
+  "acc A s r ps (x#xs) zs =
             (let t = next A x s
              in if fin A t
-                then acc A t (acc A (start A) ([],xs) xs [] [])
-                         xs (zs@[x]) (zs@[x])
-                else acc A t r xs ys (zs@[x]))"
+                then acc A t (acc A (start A) ([],xs) [] xs [])
+                         (zs@[x]) xs (zs@[x])
+                else acc A t r ps xs (zs@[x]))"
 
 constdefs
  auto_chopper :: ('a,'s)da => 'a chopper
-"auto_chopper A xs == acc A (start A) ([],xs) xs [] []"
+"auto_chopper A xs == acc A (start A) ([],xs) [] xs []"
 
 (* acc_prefix is an auxiliary notion for the proof *)
 constdefs