src/HOL/simpdata.ML
changeset 4930 89271bc4e7ed
parent 4830 bd73675adbed
child 5190 4ae031622592
     1.1 --- a/src/HOL/simpdata.ML	Thu May 14 16:44:04 1998 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Thu May 14 16:50:09 1998 +0200
     1.3 @@ -346,15 +346,16 @@
     1.4  infix 4 addsplits delsplits;
     1.5  
     1.6  fun ss addsplits splits =
     1.7 -  let fun addsplit(ss,split) =
     1.8 -        let val name = "split " ^ const_of_split_thm split
     1.9 -        in ss addloop (name,split_tac [split]) end
    1.10 +  let fun addsplit (ss,split) =
    1.11 +        let val (name,asm) = split_thm_info split 
    1.12 +        in ss addloop ("split "^ name ^ (if asm then " asm" else ""),
    1.13 +		       (if asm then split_asm_tac else split_tac) [split]) end
    1.14    in foldl addsplit (ss,splits) end;
    1.15  
    1.16  fun ss delsplits splits =
    1.17    let fun delsplit(ss,split) =
    1.18 -        let val name = "split " ^ const_of_split_thm split
    1.19 -        in ss delloop name end
    1.20 +        let val (name,asm) = split_thm_info split 
    1.21 +        in ss delloop ("split "^ name ^ (if asm then " asm" else "")) end
    1.22    in foldl delsplit (ss,splits) end;
    1.23  
    1.24  fun Addsplits splits = (simpset_ref() := simpset() addsplits splits);