# HG changeset patch
# User wenzelm
# Date 1122556789 -7200
# Node ID 9ef19e3c7fdd155ca274c28a25809476d0733712
# Parent  91ded127f5f7e02f91803c2ed620cc14c1687cd5
Sign.typ_unify;

diff -r 91ded127f5f7 -r 9ef19e3c7fdd src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Jul 28 15:19:48 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Thu Jul 28 15:19:49 2005 +0200
@@ -177,7 +177,6 @@
   same type in all introduction rules*)
 fun unify_consts thy cs intr_ts =
   (let
-    val tsig = Sign.tsig_of thy;
     val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
     fun varify (t, (i, ts)) =
       let val t' = map_term_types (Logic.incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
@@ -186,12 +185,10 @@
     val (i', intr_ts') = foldr varify (i, []) intr_ts;
     val rec_consts = fold add_term_consts_2 cs' [];
     val intr_consts = fold add_term_consts_2 intr_ts' [];
-    fun unify (env, (cname, cT)) =
+    fun unify (cname, cT) =
       let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts)
-      in Library.foldl (fn ((env', j'), Tp) => (Type.unify tsig (env', j') Tp))
-          (env, (replicate (length consts) cT) ~~ consts)
-      end;
-    val (env, _) = Library.foldl unify ((Vartab.empty, i'), rec_consts);
+      in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
+    val (env, _) = fold unify rec_consts (Vartab.empty, i');
     val subst = Type.freeze o map_term_types (Envir.norm_type env)
 
   in (map subst cs', map subst intr_ts')
diff -r 91ded127f5f7 -r 9ef19e3c7fdd src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Thu Jul 28 15:19:48 2005 +0200
+++ b/src/HOL/Tools/record_package.ML	Thu Jul 28 15:19:49 2005 +0200
@@ -429,9 +429,7 @@
     val (flds,(more,_)) = split_last (Symtab.lookup_multi (extfields,name));
     val args = map varifyT (snd (#extension (valOf (Symtab.lookup (records,recname)))));
 
-    val tsig = Sign.tsig_of sg;
-    fun unify (t,env) = Type.unify tsig env t;
-    val (subst,_) = foldr unify (Vartab.empty,0) (but_last args ~~ but_last Ts);
+    val (subst,_) = fold (Sign.typ_unify sg) (but_last args ~~ but_last Ts) (Vartab.empty,0);
     val flds' = map (apsnd ((Envir.norm_type subst) o varifyT)) flds;
   in (flds',(more,moreT)) end;
 
@@ -570,12 +568,10 @@
                               | NONE => Sign.defaultS sg);
     
  
-    val tsig = Sign.tsig_of sg;
-    fun to_type t = Type.cert_typ tsig 
+    fun to_type t = Sign.certify_typ sg
                        (Sign.intern_typ sg 
                          (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t));
-    fun unify (t,env) = Type.unify tsig env t; 
-    
+
     fun mk_ext (fargs as (name,arg)::_) =
          (case get_fieldext sg (Sign.intern_const sg name) of
             SOME (ext,alphas) => 
@@ -587,9 +583,10 @@
                        val (args,rest) = splitargs (map fst flds') fargs;
                        val vartypes = map Type.varifyT types;
                        val argtypes = map to_type args;
-                       val (subst,_) = foldr unify (Vartab.empty,0) (vartypes ~~ argtypes);
+                       val (subst,_) = fold (Sign.typ_unify sg) (vartypes ~~ argtypes)
+                                            (Vartab.empty,0);
                        val alphas' = map ((Syntax.term_of_typ (! Syntax.show_sorts)) o 
-                                          (Envir.norm_type subst) o Type.varifyT) 
+                                          Envir.norm_type subst o Type.varifyT) 
                                          (but_last alphas);
  
                        val more' = mk_ext rest;   
@@ -727,13 +724,12 @@
       
       val T = fixT (Sign.intern_typ sg 
                       (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm)); 
-      val tsig = Sign.tsig_of sg
 
       fun mk_type_abbr subst name alphas = 
           let val abbrT = Type (name, map (fn a => TVar ((a, 0), Sign.defaultS sg)) alphas);
           in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;    
 
-      fun unify rT T = fst (Type.unify tsig (Vartab.empty,0) (Type.varifyT rT,T));
+      fun unify rT T = fst (Sign.typ_unify sg (Type.varifyT rT,T) (Vartab.empty,0));
 
    in if !print_record_type_abbr
       then (case last_extT T of
@@ -760,9 +756,6 @@
 
     val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t)
 
-    val tsig = Sign.tsig_of sg
-    fun unify (t,v) = Type.unify tsig v t;
-
     fun term_of_type T = Syntax.term_of_typ (!Syntax.show_sorts) (Sign.extern_typ sg T);
  
     fun field_lst T =
@@ -780,8 +773,9 @@
                                             ::map (apfst NameSpace.base) fs; 
                                 val (args',more) = split_last args; 
                                 val alphavars = map Type.varifyT (but_last alphas); 
-                                val (subst,_)= foldr unify (Vartab.empty,0) (alphavars~~args');
-                                val flds'' =map (apsnd ((Envir.norm_type subst)o(Type.varifyT)))
+                                val (subst,_)= fold (Sign.typ_unify sg) (alphavars~~args')
+                                                    (Vartab.empty,0);
+                                val flds'' =map (apsnd (Envir.norm_type subst o Type.varifyT))
                                                 flds';
                               in flds''@field_lst more end
                               handle TUNIFY         => [("",T)] 
diff -r 91ded127f5f7 -r 9ef19e3c7fdd src/Pure/IsaPlanner/term_lib.ML
--- a/src/Pure/IsaPlanner/term_lib.ML	Thu Jul 28 15:19:48 2005 +0200
+++ b/src/Pure/IsaPlanner/term_lib.ML	Thu Jul 28 15:19:49 2005 +0200
@@ -159,9 +159,8 @@
       (* is it OK to ignore the type instantiation info? 
          or should I be using it? *)
       val typs_unify = 
-          (SOME (Type.unify (Sign.tsig_of sgn) (Term.Vartab.empty, ix) 
-                            (pat_ty, tgt_ty)))
-          handle Type.TUNIFY => NONE;
+          SOME (Sign.typ_unify sgn (pat_ty, tgt_ty) (Term.Vartab.empty, ix))
+            handle Type.TUNIFY => NONE;
     in
       case typs_unify of
         SOME (typinsttab, ix2) =>
@@ -691,4 +690,4 @@
     | change_frees_to_vars l = l;
 
 
-end;
\ No newline at end of file
+end;
diff -r 91ded127f5f7 -r 9ef19e3c7fdd src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Jul 28 15:19:48 2005 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Jul 28 15:19:49 2005 +0200
@@ -247,7 +247,7 @@
     val U = Term.fastype_of u;
     val maxidx' = Int.max (maxidx, Int.max (#2 xi, Term.maxidx_of_term u));
   in
-    Type.unify (Sign.tsig_of thy) (unifier, maxidx') (T, U)
+    Sign.typ_unify thy (T, U) (unifier, maxidx')
       handle Type.TUNIFY => error_var "Incompatible type for instantiation of " xi
   end;
 
diff -r 91ded127f5f7 -r 9ef19e3c7fdd src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Thu Jul 28 15:19:48 2005 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Thu Jul 28 15:19:49 2005 +0200
@@ -62,7 +62,7 @@
 fun unifyT sg env T U =
   let
     val Envir.Envir {asol, iTs, maxidx} = env;
-    val (iTs', maxidx') = Type.unify (Sign.tsig_of sg) (iTs, maxidx) (T, U)
+    val (iTs', maxidx') = Sign.typ_unify sg (T, U) (iTs, maxidx)
   in Envir.Envir {asol=asol, iTs=iTs', maxidx=maxidx'} end
   handle Type.TUNIFY => error ("Non-unifiable types:\n" ^
     Sign.string_of_typ sg T ^ "\n\n" ^ Sign.string_of_typ sg U);
diff -r 91ded127f5f7 -r 9ef19e3c7fdd src/Pure/unify.ML
--- a/src/Pure/unify.ML	Thu Jul 28 15:19:48 2005 +0200
+++ b/src/Pure/unify.ML	Thu Jul 28 15:19:49 2005 +0200
@@ -176,7 +176,7 @@
 
 fun unify_types thy (T,U, env as Envir.Envir{asol,iTs,maxidx}) =
   if T=U then env
-  else let val (iTs',maxidx') = Type.unify (Sign.tsig_of thy) (iTs, maxidx) (U, T)
+  else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx)
        in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
        handle Type.TUNIFY => raise CANTUNIFY;