diff -r 5e82d6cafb5f -r 2955ee2424ce src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Mon Nov 06 22:49:16 2000 +0100
+++ b/src/Provers/splitter.ML	Mon Nov 06 22:50:01 2000 +0100
@@ -208,7 +208,7 @@
               Const(c, cT) =>
                 let fun find [] = []
                       | find ((gcT, thm, T, n)::tups) =
-                          if Type.typ_instance(Sign.tsig_of sg, cT, gcT)
+                          if Sign.typ_instance 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)