--- a/src/HOL/simpdata.ML Thu May 14 16:44:04 1998 +0200
+++ b/src/HOL/simpdata.ML Thu May 14 16:50:09 1998 +0200
@@ -346,15 +346,16 @@
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 ("split "^ 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 = "split " ^ const_of_split_thm split
- in ss delloop name end
+ let val (name,asm) = split_thm_info split
+ in ss delloop ("split "^ name ^ (if asm then " asm" else "")) end
in foldl delsplit (ss,splits) end;
fun Addsplits splits = (simpset_ref() := simpset() addsplits splits);