src/FOL/simpdata.ML

--- a/src/FOL/simpdata.ML	Thu May 14 16:44:04 1998 +0200
+++ b/src/FOL/simpdata.ML	Thu May 14 16:50:09 1998 +0200
@@ -264,13 +264,20 @@
 fun Addcongs congs = (simpset_ref() := simpset() addcongs congs);
 fun Delcongs congs = (simpset_ref() := simpset() delcongs congs);
 
-infix 4 addsplits;
+infix 4 addsplits delsplits;
 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
+  let fun addsplit (ss,split) =
+        let val (name,asm) = split_thm_info split 
+        in ss addloop (name ^ (if asm then " asm" else ""),
+		       (if asm then split_asm_tac else split_tac) [split]) end
   in foldl addsplit (ss,splits) end;
 
+fun ss delsplits splits =
+  let fun delsplit(ss,split) =
+        let val (name,asm) = split_thm_info split 
+        in ss delloop (name ^ (if asm then " asm" else "")) end
+  in foldl delsplit (ss,splits) end;
+
 val IFOL_simps =
    [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
     imp_simps @ iff_simps @ quant_simps;