# HG changeset patch
# User nipkow
# Date 889532615 -3600
# Node ID facfbbca724289c5030d3982605c098ae22d26cd
# Parent  75a9ef36b1fe0e87cf5d6574de2a4cd96e361f99
Removed expand_split from simpset.

diff -r 75a9ef36b1fe -r facfbbca7242 src/HOL/Lex/AutoChopper1.thy
--- a/src/HOL/Lex/AutoChopper1.thy	Mon Mar 09 16:30:55 1998 +0100
+++ b/src/HOL/Lex/AutoChopper1.thy	Tue Mar 10 13:23:35 1998 +0100
@@ -25,7 +25,7 @@
 recdef acc "inv_image (less_than ** less_than)
               (%(A,ys,s,xss,zs,xs). (length xs + length ys + length zs,
                                      length ys))"
-simpset "simpset() addsimps (less_add_Suc2::add_ac) addsplits [expand_if]"
+simpset "simpset() addsimps (less_add_Suc2::add_ac)"
 "acc(A,[],s,xss,zs,[]) = (xss, zs)"
 "acc(A,[],s,xss,zs,x#xs) = acc(A,zs,start A, xss @ [x#xs],[],[])"
 "acc(A,y#ys,s,xss,zs,xs) =
diff -r 75a9ef36b1fe -r facfbbca7242 src/HOL/Lex/ROOT.ML
--- a/src/HOL/Lex/ROOT.ML	Mon Mar 09 16:30:55 1998 +0100
+++ b/src/HOL/Lex/ROOT.ML	Tue Mar 10 13:23:35 1998 +0100
@@ -8,4 +8,5 @@
 
 use_thy"AutoChopper";
 use_thy"AutoChopper1";
+use_thy"AutoMaxChop";
 use_thy"Regset_of_auto";