src/Provers/splitter.ML
changeset 13859 adf68d9e5dec
parent 13855 644692eca537
child 14854 61bdf2ae4dc5
     1.1 --- a/src/Provers/splitter.ML	Tue Mar 11 15:19:27 2003 +0100
     1.2 +++ b/src/Provers/splitter.ML	Thu Mar 13 18:54:38 2003 +0100
     1.3 @@ -409,22 +409,24 @@
     1.4  
     1.5  (* addsplits / delsplits *)
     1.6  
     1.7 -fun split_name sg (name, T) asm = "split " ^ 
     1.8 -  (if asm then "asm " else "") ^ name ^ " :: " ^
     1.9 -  Sign.string_of_typ sg (typ_subst_TVars
    1.10 -    (map (rpair dummyT o fst) (typ_tvars T)) T);
    1.11 +fun string_of_typ (Type (s, Ts)) = (if null Ts then ""
    1.12 +      else enclose "(" ")" (commas (map string_of_typ Ts))) ^ s
    1.13 +  | string_of_typ _ = "_";
    1.14 +
    1.15 +fun split_name (name, T) asm = "split " ^ 
    1.16 +  (if asm then "asm " else "") ^ name ^ " :: " ^ string_of_typ T;
    1.17  
    1.18  fun ss addsplits splits =
    1.19    let fun addsplit (ss,split) =
    1.20          let val (name,asm) = split_thm_info split
    1.21 -        in Simplifier.addloop (ss, (split_name (sign_of_thm split) name asm,
    1.22 +        in Simplifier.addloop (ss, (split_name name asm,
    1.23  		       (if asm then split_asm_tac else split_tac) [split])) end
    1.24    in foldl addsplit (ss,splits) end;
    1.25  
    1.26  fun ss delsplits splits =
    1.27    let fun delsplit(ss,split) =
    1.28          let val (name,asm) = split_thm_info split
    1.29 -        in Simplifier.delloop (ss, split_name (sign_of_thm split) name asm)
    1.30 +        in Simplifier.delloop (ss, split_name name asm)
    1.31    end in foldl delsplit (ss,splits) end;
    1.32  
    1.33  fun Addsplits splits = (Simplifier.simpset_ref() :=