# HG changeset patch
# User nipkow
# Date 916316402 -3600
# Node ID 30b84ad2131dd94c4b75dbd758939c9f83b25c64
# Parent  0f5ecd633c2f4d0cb6b2adabdb1ceed2fc9b99a3
Fixed old bug: selection of constant to be split should depend not just on
the name but also on the type.

diff -r 0f5ecd633c2f -r 30b84ad2131d src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Thu Jan 14 13:19:12 1999 +0100
+++ b/src/Provers/splitter.ML	Thu Jan 14 13:20:02 1999 +0100
@@ -185,23 +185,28 @@
    t    : the term to be scanned
 ******************************************************************************)
 
-fun split_posns cmap Ts t =
-  let fun posns Ts pos apsns (Abs(_,T,t)) =
-            let val U = fastype_of1(T::Ts,t)
-            in posns (T::Ts) (0::pos) ((T,U,pos)::apsns) t end
-        | posns Ts pos apsns t =
-            let val (h,ts) = strip_comb t
-                fun iter((i,a),t) = (i+1, (posns Ts (i::pos) apsns t) @ a);
-                val a = case h of
-                  Const(c,_) =>
-                    (case assoc(cmap,c) of
-                       Some(thm, T, n) =>
-                         let val t2 = list_comb (h, take (n, ts)) in
-                           mk_split_pack(thm,T,n,ts,apsns,pos,type_of1(Ts, t2),t2)
-                         end
-                     | None => [])
-                | _ => []
-             in snd(foldl iter ((0,a),ts)) end
+fun split_posns cmap sg Ts t =
+  let
+    fun posns Ts pos apsns (Abs(_,T,t)) =
+          let val U = fastype_of1(T::Ts,t)
+          in posns (T::Ts) (0::pos) ((T,U,pos)::apsns) t end
+      | posns Ts pos apsns t =
+          let
+            val (h,ts) = strip_comb t
+            fun iter((i,a),t) = (i+1, (posns Ts (i::pos) apsns t) @ a);
+            val a = case h of
+              Const(c,cT) =>
+                (case assoc(cmap,c) of
+                   Some(gcT, thm, T, n) =>
+                     if Type.typ_instance(Sign.tsig_of sg, cT, gcT)
+                     then
+                       let val t2 = list_comb (h, take (n, ts))
+                       in mk_split_pack(thm,T,n,ts,apsns,pos,type_of1(Ts, t2),t2)
+                       end
+                     else []
+                 | None => [])
+            | _ => []
+          in snd(foldl iter ((0,a),ts)) end
   in posns Ts [] [] t end;
 
 
@@ -218,10 +223,11 @@
 *************************************************************)
 
 fun select cmap state i =
-  let val goali = nth_subgoal i state
+  let val sg = #sign(rep_thm state)
+      val goali = nth_subgoal i state
       val Ts = rev(map #2 (Logic.strip_params goali))
       val _ $ t $ _ = Logic.strip_assums_concl goali;
-  in (Ts,t, sort shorter (split_posns cmap Ts t)) end;
+  in (Ts,t, sort shorter (split_posns cmap sg Ts t)) end;
 
 
 (*************************************************************
@@ -291,8 +297,8 @@
   let val splits = map Data.mk_eq splits;
       fun const(thm) =
             (case concl_of thm of _$(t as _$lhs)$_ =>
-               (case strip_comb lhs of (Const(a,_),args) =>
-                  (a,(thm,fastype_of t,length args))
+               (case strip_comb lhs of (Const(a,aT),args) =>
+                  (a,(aT,thm,fastype_of t,length args))
                 | _ => split_format_err())
              | _ => split_format_err())
       val cmap = map const splits;