diff -r fca9cd9fd115 -r 291ce4c4b50e src/HOL/Lex/AutoChopper.thy
--- a/src/HOL/Lex/AutoChopper.thy	Wed Oct 25 18:36:01 2000 +0200
+++ b/src/HOL/Lex/AutoChopper.thy	Wed Oct 25 18:39:01 2000 +0200
@@ -19,7 +19,7 @@
 its antecedents.
 *)
 
-AutoChopper = Prefix + DA + Chopper +
+AutoChopper = DA + Chopper +
 
 constdefs
  is_auto_chopper :: (('a,'s)da => 'a chopper) => bool