--- 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')
--- 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)]
--- 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;
--- 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;
--- 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);
--- 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;