# HG changeset patch
# User nipkow
# Date 962890619 -7200
# Node ID dbf30a2d1b565947cb4bb36943feae0da3f4adb7
# Parent  1b917b8b1b38a7d7d6fac1197b82858e001fe781
Now two split thms for same constant at different types is allowed.

diff -r 1b917b8b1b38 -r dbf30a2d1b56 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Thu Jul 06 15:01:52 2000 +0200
+++ b/src/Provers/splitter.ML	Thu Jul 06 15:36:59 2000 +0200
@@ -206,15 +206,15 @@
             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, T', n, ts, apsns, pos, type_of1 (Ts, t2), t2)
-                       end
-                     else []
-                 | None => [])
+                let fun find [] = []
+                      | find ((gcT, thm, T, n)::tups) =
+                          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,T',n,ts,apsns,pos,type_of1(Ts,t2),t2)
+                            end
+                          else find tups
+                in find (assocs cmap c) end
             | _ => []
           in snd(foldl iter ((0, a), ts)) end
   in posns Ts [] [] t end;
@@ -301,13 +301,17 @@
 fun split_tac [] i = no_tac
   | split_tac splits i =
   let val splits = map Data.mk_eq splits;
-      fun const(thm) =
+      fun add_thm(cmap,thm) =
             (case concl_of thm of _$(t as _$lhs)$_ =>
                (case strip_comb lhs of (Const(a,aT),args) =>
-                  (a,(aT,thm,fastype_of t,length args))
+                  let val info = (aT,thm,fastype_of t,length args)
+                  in case assoc(cmap,a) of
+                       Some infos => overwrite(cmap,(a,info::infos))
+                     | None => (a,[info])::cmap
+                  end
                 | _ => split_format_err())
              | _ => split_format_err())
-      val cmap = map const splits;
+      val cmap = foldl add_thm ([],splits);
       fun lift_tac Ts t p st = rtac (inst_lift Ts t p st i) i st
       fun lift_split_tac state =
             let val (Ts, t, splits) = select cmap state i