diff -r ba267836dd7a -r 2ce2e659c2b1 src/HOL/Lex/AutoChopper.thy
--- a/src/HOL/Lex/AutoChopper.thy	Tue Nov 04 20:52:20 1997 +0100
+++ b/src/HOL/Lex/AutoChopper.thy	Wed Nov 05 09:08:35 1997 +0100
@@ -12,6 +12,8 @@
 
 WARNING: auto_chopper is exponential(?)
 if the recursive calls in the penultimate argument are evaluated eagerly.
+
+A more efficient version is defined in AutoChopper1.
 *)
 
 AutoChopper = Auto + Chopper +
@@ -39,32 +41,3 @@
                 else acc xs (nxt st x) ys (zs@[x]) chopsr A)"
 
 end
-
-(* The following definition of acc should also work:
-consts
-  acc1 :: [('a,'b)auto, 'a list, 'b, 'a list list, 'a list, 'a list]
-          => 'a list list * 'a list
-
-acc1 A [] s xss zs xs =
-  (if xs=[] then (xss, zs)
-   else acc1 A zs (start A) (xss @ [xs]) [] [])
-acc1 A (y#ys) s xss zs rec =
-  let s' = next A s;
-      zs' = (if fin A s' then [] else zs@[y])
-      xs' = (if fin A s' then xs@zs@[y] else xs)
-  in acc1 A ys s' xss zs' xs'
-
-Advantage: does not need lazy evaluation for reasonable (quadratic)
-performance.
-
-Disadavantage: not primrec.
-  
-Termination measure:
-  size(A,ys,s,xss,zs,rec) = (|xs| + |ys| + |zs|, |ys|)
-
-Termination proof: the first clause reduces the first component by |xs|,
-the second clause leaves the first component alone but reduces the second by 1.
-
-Claim: acc1 A xs s [] [] [] = acc xs s [] [] ([],xs) A
-Generalization?
-*)