# HG changeset patch
# User nipkow
# Date 888676877 -3600
# Node ID 06f3c56dcba8d8b21f9c0abb047da0e138930811
# Parent  131989b78417ee8af2b877a5d7f52dedbf482377
Splitters via named loopers.

diff -r 131989b78417 -r 06f3c56dcba8 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Sat Feb 28 15:40:50 1998 +0100
+++ b/src/FOL/simpdata.ML	Sat Feb 28 15:41:17 1998 +0100
@@ -267,7 +267,11 @@
 fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
 
 infix 4 addsplits;
-fun ss addsplits splits = ss addloop (split_tac splits);
+fun ss addsplits splits =
+  let fun addsplit(ss,split) =
+        let val name = "split " ^ const_of_split_thm split
+        in ss addloop (name,split_tac [split]) end
+  in foldl addsplit (ss,splits) end;
 
 val IFOL_simps =
    [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
diff -r 131989b78417 -r 06f3c56dcba8 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Sat Feb 28 15:40:50 1998 +0100
+++ b/src/HOL/simpdata.ML	Sat Feb 28 15:41:17 1998 +0100
@@ -337,8 +337,11 @@
 			(disjE,conjE,exE,contrapos,contrapos2,notnotD);
 
 infix 4 addsplits;
-fun ss addsplits splits = ss addloop (split_tac splits);
-
+fun ss addsplits splits =
+  let fun addsplit(ss,split) =
+        let val name = "split " ^ const_of_split_thm split
+        in ss addloop (name,split_tac [split]) end
+  in foldl addsplit (ss,splits) end;
 
 qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
   (K [split_tac [expand_if] 1, blast_tac HOL_cs 1]);