# HG changeset patch
# User berghofe
# Date 1047388400 -3600
# Node ID 644692eca537830eb1bee3e8cb03e83c1eb91758
# Parent  91c9ab25fecea8ce9151f3af415be912c19f9992
addsplits / delsplits no longer ignore type of constant.

diff -r 91c9ab25fece -r 644692eca537 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Mon Mar 10 17:25:34 2003 +0100
+++ b/src/Provers/splitter.ML	Tue Mar 11 14:13:20 2003 +0100
@@ -57,11 +57,10 @@
 fun split_format_err() = error("Wrong format for split rule");
 
 fun split_thm_info thm = case concl_of (Data.mk_eq thm) of
-     Const("==", _)$(Var _$t)$c =>
-        (case strip_comb t of
-           (Const(a,_),_) => (a,case c of (Const(s,_)$_)=>s=const_not|_=> false)
-         | _              => split_format_err())
-   | _ => split_format_err();
+     Const("==", _) $ (Var _ $ t) $ c => (case strip_comb t of
+       (Const p, _) => (p, case c of (Const (s, _) $ _) => s = const_not | _ => false)
+     | _ => split_format_err ())
+   | _ => split_format_err ();
 
 fun mk_case_split_tac order =
 let
@@ -371,7 +370,7 @@
 fun split_asm_tac []     = K no_tac
   | split_asm_tac splits = 
 
-  let val cname_list = map (fst o split_thm_info) splits;
+  let val cname_list = map (fst o fst o split_thm_info) splits;
       fun is_case (a,_) = a mem cname_list;
       fun tac (t,i) = 
 	  let val n = find_index (exists_Const is_case) 
@@ -410,19 +409,22 @@
 
 (* addsplits / delsplits *)
 
-fun split_name name asm = "split " ^ name ^ (if asm then " asm" else "");
+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 ss addsplits splits =
   let fun addsplit (ss,split) =
         let val (name,asm) = split_thm_info split
-        in Simplifier.addloop(ss,(split_name name asm,
+        in Simplifier.addloop (ss, (split_name (sign_of_thm split) 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 name asm)
+        in Simplifier.delloop (ss, split_name (sign_of_thm split) name asm)
   end in foldl delsplit (ss,splits) end;
 
 fun Addsplits splits = (Simplifier.simpset_ref() :=