# HG changeset patch
# User wenzelm
# Date 973547401 -3600
# Node ID 2955ee2424ce826ba9b5ce2889c84425a8927d5d
# Parent  5e82d6cafb5fd8a0e49f38d3c1d141492db60fc9
Sign.typ_instance;

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)
diff -r 5e82d6cafb5f -r 2955ee2424ce src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Nov 06 22:49:16 2000 +0100
+++ b/src/Pure/drule.ML	Mon Nov 06 22:50:01 2000 +0100
@@ -178,7 +178,7 @@
   error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
 
 fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
-let val {tsig,...} = Sign.rep_sg sign
+let
     fun split([],tvs,vs) = (tvs,vs)
       | split((sv,st)::l,tvs,vs) = (case Symbol.explode sv of
                   "'"::cs => split(l,(Syntax.indexname cs,st)::tvs,vs)
@@ -188,7 +188,7 @@
         let val ixn = ("'" ^ a,i);
             val S = case rsorts ixn of Some S => S | None => absent ixn;
             val T = Sign.read_typ (sign,sorts) st;
-        in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
+        in if Sign.typ_instance sign (T, TVar(ixn,S)) then (ixn,T)
            else inst_failure ixn
         end
     val tye = map readT tvs;
@@ -654,12 +654,11 @@
         val maxi = Int.max(maxidx, Int.max(maxt, maxu));
         val sign' = Sign.merge(sign, Sign.merge(signt, signu))
         val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U)
-          handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u])
+          handle Type.TUNIFY => raise TYPE("Ill-typed instantiation", [T,U], [t,u])
     in  (sign', tye', maxi')  end;
 in
 fun cterm_instantiate ctpairs0 th =
   let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th), Vartab.empty, 0))
-      val tsig = #tsig(Sign.rep_sg sign);
       fun instT(ct,cu) = let val inst = subst_TVars_Vartab tye
                          in (cterm_fun inst ct, cterm_fun inst cu) end
       fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
diff -r 5e82d6cafb5f -r 2955ee2424ce src/Pure/theory.ML
--- a/src/Pure/theory.ML	Mon Nov 06 22:49:16 2000 +0100
+++ b/src/Pure/theory.ML	Mon Nov 06 22:50:01 2000 +0100
@@ -324,12 +324,9 @@
 datatype overloading = NoOverloading | Useless | Plain;
 
 fun overloading sg declT defT =
-  let
-    val tsig = Sign.tsig_of sg;
-    val T = Term.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT);
-  in
-    if Type.typ_instance (tsig, declT, T) then NoOverloading
-    else if Type.typ_instance (tsig, Type.rem_sorts declT, Type.rem_sorts T) then Useless
+  let val T = Term.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT) in
+    if Sign.typ_instance sg (declT, T) then NoOverloading
+    else if Sign.typ_instance sg (Type.rem_sorts declT, Type.rem_sorts T) then Useless
     else Plain
   end;