1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Jul 28 15:19:48 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Jul 28 15:19:49 2005 +0200
     1.3 @@ -177,7 +177,6 @@
     1.4    same type in all introduction rules*)
     1.5  fun unify_consts thy cs intr_ts =
     1.6    (let
     1.7 -    val tsig = Sign.tsig_of thy;
     1.8      val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
     1.9      fun varify (t, (i, ts)) =
    1.10        let val t' = map_term_types (Logic.incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
    1.11 @@ -186,12 +185,10 @@
    1.12      val (i', intr_ts') = foldr varify (i, []) intr_ts;
    1.13      val rec_consts = fold add_term_consts_2 cs' [];
    1.14      val intr_consts = fold add_term_consts_2 intr_ts' [];
    1.15 -    fun unify (env, (cname, cT)) =
    1.16 +    fun unify (cname, cT) =
    1.17        let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts)
    1.18 -      in Library.foldl (fn ((env', j'), Tp) => (Type.unify tsig (env', j') Tp))
    1.19 -          (env, (replicate (length consts) cT) ~~ consts)
    1.20 -      end;
    1.21 -    val (env, _) = Library.foldl unify ((Vartab.empty, i'), rec_consts);
    1.22 +      in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
    1.23 +    val (env, _) = fold unify rec_consts (Vartab.empty, i');
    1.24      val subst = Type.freeze o map_term_types (Envir.norm_type env)
    1.25  
    1.26    in (map subst cs', map subst intr_ts')

     2.1 --- a/src/HOL/Tools/record_package.ML	Thu Jul 28 15:19:48 2005 +0200
     2.2 +++ b/src/HOL/Tools/record_package.ML	Thu Jul 28 15:19:49 2005 +0200
     2.3 @@ -429,9 +429,7 @@
     2.4      val (flds,(more,_)) = split_last (Symtab.lookup_multi (extfields,name));
     2.5      val args = map varifyT (snd (#extension (valOf (Symtab.lookup (records,recname)))));
     2.6  
     2.7 -    val tsig = Sign.tsig_of sg;
     2.8 -    fun unify (t,env) = Type.unify tsig env t;
     2.9 -    val (subst,_) = foldr unify (Vartab.empty,0) (but_last args ~~ but_last Ts);
    2.10 +    val (subst,_) = fold (Sign.typ_unify sg) (but_last args ~~ but_last Ts) (Vartab.empty,0);
    2.11      val flds' = map (apsnd ((Envir.norm_type subst) o varifyT)) flds;
    2.12    in (flds',(more,moreT)) end;
    2.13  
    2.14 @@ -570,12 +568,10 @@
    2.15                                | NONE => Sign.defaultS sg);
    2.16      
    2.17   
    2.18 -    val tsig = Sign.tsig_of sg;
    2.19 -    fun to_type t = Type.cert_typ tsig 
    2.20 +    fun to_type t = Sign.certify_typ sg
    2.21                         (Sign.intern_typ sg 
    2.22                           (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t));
    2.23 -    fun unify (t,env) = Type.unify tsig env t; 
    2.24 -    
    2.25 +
    2.26      fun mk_ext (fargs as (name,arg)::_) =
    2.27           (case get_fieldext sg (Sign.intern_const sg name) of
    2.28              SOME (ext,alphas) => 
    2.29 @@ -587,9 +583,10 @@
    2.30                         val (args,rest) = splitargs (map fst flds') fargs;
    2.31                         val vartypes = map Type.varifyT types;
    2.32                         val argtypes = map to_type args;
    2.33 -                       val (subst,_) = foldr unify (Vartab.empty,0) (vartypes ~~ argtypes);
    2.34 +                       val (subst,_) = fold (Sign.typ_unify sg) (vartypes ~~ argtypes)
    2.35 +                                            (Vartab.empty,0);
    2.36                         val alphas' = map ((Syntax.term_of_typ (! Syntax.show_sorts)) o 
    2.37 -                                          (Envir.norm_type subst) o Type.varifyT) 
    2.38 +                                          Envir.norm_type subst o Type.varifyT) 
    2.39                                           (but_last alphas);
    2.40   
    2.41                         val more' = mk_ext rest;   
    2.42 @@ -727,13 +724,12 @@
    2.43        
    2.44        val T = fixT (Sign.intern_typ sg 
    2.45                        (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm)); 
    2.46 -      val tsig = Sign.tsig_of sg
    2.47  
    2.48        fun mk_type_abbr subst name alphas = 
    2.49            let val abbrT = Type (name, map (fn a => TVar ((a, 0), Sign.defaultS sg)) alphas);
    2.50            in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;    
    2.51  
    2.52 -      fun unify rT T = fst (Type.unify tsig (Vartab.empty,0) (Type.varifyT rT,T));
    2.53 +      fun unify rT T = fst (Sign.typ_unify sg (Type.varifyT rT,T) (Vartab.empty,0));
    2.54  
    2.55     in if !print_record_type_abbr
    2.56        then (case last_extT T of
    2.57 @@ -760,9 +756,6 @@
    2.58  
    2.59      val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t)
    2.60  
    2.61 -    val tsig = Sign.tsig_of sg
    2.62 -    fun unify (t,v) = Type.unify tsig v t;
    2.63 -
    2.64      fun term_of_type T = Syntax.term_of_typ (!Syntax.show_sorts) (Sign.extern_typ sg T);
    2.65   
    2.66      fun field_lst T =
    2.67 @@ -780,8 +773,9 @@
    2.68                                              ::map (apfst NameSpace.base) fs; 
    2.69                                  val (args',more) = split_last args; 
    2.70                                  val alphavars = map Type.varifyT (but_last alphas); 
    2.71 -                                val (subst,_)= foldr unify (Vartab.empty,0) (alphavars~~args');
    2.72 -                                val flds'' =map (apsnd ((Envir.norm_type subst)o(Type.varifyT)))
    2.73 +                                val (subst,_)= fold (Sign.typ_unify sg) (alphavars~~args')
    2.74 +                                                    (Vartab.empty,0);
    2.75 +                                val flds'' =map (apsnd (Envir.norm_type subst o Type.varifyT))
    2.76                                                  flds';
    2.77                                in flds''@field_lst more end
    2.78                                handle TUNIFY         => [("",T)] 

     3.1 --- a/src/Pure/IsaPlanner/term_lib.ML	Thu Jul 28 15:19:48 2005 +0200
     3.2 +++ b/src/Pure/IsaPlanner/term_lib.ML	Thu Jul 28 15:19:49 2005 +0200
     3.3 @@ -159,9 +159,8 @@
     3.4        (* is it OK to ignore the type instantiation info? 
     3.5           or should I be using it? *)
     3.6        val typs_unify = 
     3.7 -          (SOME (Type.unify (Sign.tsig_of sgn) (Term.Vartab.empty, ix) 
     3.8 -                            (pat_ty, tgt_ty)))
     3.9 -          handle Type.TUNIFY => NONE;
    3.10 +          SOME (Sign.typ_unify sgn (pat_ty, tgt_ty) (Term.Vartab.empty, ix))
    3.11 +            handle Type.TUNIFY => NONE;
    3.12      in
    3.13        case typs_unify of
    3.14          SOME (typinsttab, ix2) =>
    3.15 @@ -691,4 +690,4 @@
    3.16      | change_frees_to_vars l = l;
    3.17  
    3.18  
    3.19 -end;
    3.20 \ No newline at end of file
    3.21 +end;

     4.1 --- a/src/Pure/Isar/attrib.ML	Thu Jul 28 15:19:48 2005 +0200
     4.2 +++ b/src/Pure/Isar/attrib.ML	Thu Jul 28 15:19:49 2005 +0200
     4.3 @@ -247,7 +247,7 @@
     4.4      val U = Term.fastype_of u;
     4.5      val maxidx' = Int.max (maxidx, Int.max (#2 xi, Term.maxidx_of_term u));
     4.6    in
     4.7 -    Type.unify (Sign.tsig_of thy) (unifier, maxidx') (T, U)
     4.8 +    Sign.typ_unify thy (T, U) (unifier, maxidx')
     4.9        handle Type.TUNIFY => error_var "Incompatible type for instantiation of " xi
    4.10    end;
    4.11  

     5.1 --- a/src/Pure/Proof/reconstruct.ML	Thu Jul 28 15:19:48 2005 +0200
     5.2 +++ b/src/Pure/Proof/reconstruct.ML	Thu Jul 28 15:19:49 2005 +0200
     5.3 @@ -62,7 +62,7 @@
     5.4  fun unifyT sg env T U =
     5.5    let
     5.6      val Envir.Envir {asol, iTs, maxidx} = env;
     5.7 -    val (iTs', maxidx') = Type.unify (Sign.tsig_of sg) (iTs, maxidx) (T, U)
     5.8 +    val (iTs', maxidx') = Sign.typ_unify sg (T, U) (iTs, maxidx)
     5.9    in Envir.Envir {asol=asol, iTs=iTs', maxidx=maxidx'} end
    5.10    handle Type.TUNIFY => error ("Non-unifiable types:\n" ^
    5.11      Sign.string_of_typ sg T ^ "\n\n" ^ Sign.string_of_typ sg U);

     6.1 --- a/src/Pure/unify.ML	Thu Jul 28 15:19:48 2005 +0200
     6.2 +++ b/src/Pure/unify.ML	Thu Jul 28 15:19:49 2005 +0200
     6.3 @@ -176,7 +176,7 @@
     6.4  
     6.5  fun unify_types thy (T,U, env as Envir.Envir{asol,iTs,maxidx}) =
     6.6    if T=U then env
     6.7 -  else let val (iTs',maxidx') = Type.unify (Sign.tsig_of thy) (iTs, maxidx) (U, T)
     6.8 +  else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx)
     6.9         in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
    6.10         handle Type.TUNIFY => raise CANTUNIFY;
    6.11