# HG changeset patch
# User berghofe
# Date 1047578078 -3600
# Node ID adf68d9e5dec8ba3b8c46d80182efe38d9b302a0
# Parent  a077513c9a07828f4bf7e82c4b6c3e21975268e7
split_name no longer uses Sign.string_of_typ to encode types, since
this depends on the print mode and may lead to unpredictable results.

diff -r a077513c9a07 -r adf68d9e5dec src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Tue Mar 11 15:19:27 2003 +0100
+++ b/src/Provers/splitter.ML	Thu Mar 13 18:54:38 2003 +0100
@@ -409,22 +409,24 @@
 
 (* addsplits / delsplits *)
 
-fun split_name sg (name, T) asm = "split " ^ 
-  (if asm then "asm " else "") ^ name ^ " :: " ^
-  Sign.string_of_typ sg (typ_subst_TVars
-    (map (rpair dummyT o fst) (typ_tvars T)) T);
+fun string_of_typ (Type (s, Ts)) = (if null Ts then ""
+      else enclose "(" ")" (commas (map string_of_typ Ts))) ^ s
+  | string_of_typ _ = "_";
+
+fun split_name (name, T) asm = "split " ^ 
+  (if asm then "asm " else "") ^ name ^ " :: " ^ string_of_typ T;
 
 fun ss addsplits splits =
   let fun addsplit (ss,split) =
         let val (name,asm) = split_thm_info split
-        in Simplifier.addloop (ss, (split_name (sign_of_thm split) name asm,
+        in Simplifier.addloop (ss, (split_name name asm,
 		       (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 Simplifier.delloop (ss, split_name (sign_of_thm split) name asm)
+        in Simplifier.delloop (ss, split_name name asm)
   end in foldl delsplit (ss,splits) end;
 
 fun Addsplits splits = (Simplifier.simpset_ref() :=