# HG changeset patch
# User wenzelm
# Date 889809314 -3600
# Node ID 4469d498cd4815734b1312c6bbcdd9ba0ff29c87
# Parent  b3bfcbd9fb9304fd49c84c2860e3aac68269b6fc
moved addsplits [expand_if] from HOL_basic_ss to HOL_ss;

diff -r b3bfcbd9fb93 -r 4469d498cd48 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Mar 12 13:17:13 1998 +0100
+++ b/src/HOL/simpdata.ML	Fri Mar 13 18:15:14 1998 +0100
@@ -400,8 +400,7 @@
 			    setSSolver   safe_solver
 			    setSolver  unsafe_solver
 			    setmksimps (mksimps mksimps_pairs)
-			    setmkeqTrue mk_meta_eq_True
-                            addsplits [expand_if];
+			    setmkeqTrue mk_meta_eq_True;
 
 val HOL_ss = 
     HOL_basic_ss addsimps 
@@ -413,7 +412,8 @@
        disj_not1, not_all, not_ex, cases_simp]
      @ ex_simps @ all_simps @ simp_thms)
      addsimprocs [defALL_regroup,defEX_regroup]
-     addcongs [imp_cong];
+     addcongs [imp_cong]
+     addsplits [expand_if];
 
 qed_goal "if_distrib" HOL.thy
   "f(if c then x else y) = (if c then f x else f y)"