--- 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