tuned Type.unify;
authorwenzelm
Tue Dec 18 02:17:20 2001 +0100 (2001-12-18 ago)
changeset 12527d6c91bc3e49c
parent 12526 1b9db2581fe2
child 12528 b8bc541a4544
tuned Type.unify;
src/HOL/Tools/inductive_package.ML
src/Pure/Proof/reconstruct.ML
src/Pure/drule.ML
src/Pure/pattern.ML
src/Pure/unify.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Dec 17 14:27:18 2001 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Dec 18 02:17:20 2001 +0100
     1.3 @@ -190,7 +190,7 @@
     1.4      val intr_consts = foldl add_term_consts_2 ([], intr_ts');
     1.5      fun unify (env, (cname, cT)) =
     1.6        let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
     1.7 -      in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp))
     1.8 +      in foldl (fn ((env', j'), Tp) => (Type.unify tsig (env', j') Tp))
     1.9            (env, (replicate (length consts) cT) ~~ consts)
    1.10        end;
    1.11      val (env, _) = foldl unify ((Vartab.empty, i'), rec_consts);
     2.1 --- a/src/Pure/Proof/reconstruct.ML	Mon Dec 17 14:27:18 2001 +0100
     2.2 +++ b/src/Pure/Proof/reconstruct.ML	Tue Dec 18 02:17:20 2001 +0100
     2.3 @@ -97,7 +97,7 @@
     2.4  fun unifyT sg env T U =
     2.5    let
     2.6      val Envir.Envir {asol, iTs, maxidx} = env;
     2.7 -    val (iTs', maxidx') = Type.unify (Sign.tsig_of sg) maxidx iTs (T, U)
     2.8 +    val (iTs', maxidx') = Type.unify (Sign.tsig_of sg) (iTs, maxidx) (T, U)
     2.9    in Envir.Envir {asol=asol, iTs=iTs', maxidx=maxidx'} end
    2.10    handle Type.TUNIFY => error ("Non-unifiable types:\n" ^
    2.11      Sign.string_of_typ sg T ^ "\n\n" ^ Sign.string_of_typ sg U);
     3.1 --- a/src/Pure/drule.ML	Mon Dec 17 14:27:18 2001 +0100
     3.2 +++ b/src/Pure/drule.ML	Tue Dec 18 02:17:20 2001 +0100
     3.3 @@ -706,7 +706,7 @@
     3.4          and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
     3.5          val maxi = Int.max(maxidx, Int.max(maxt, maxu));
     3.6          val sign' = Sign.merge(sign, Sign.merge(signt, signu))
     3.7 -        val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U)
     3.8 +        val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) (tye, maxi) (T, U)
     3.9            handle Type.TUNIFY => raise TYPE("Ill-typed instantiation", [T,U], [t,u])
    3.10      in  (sign', tye', maxi')  end;
    3.11  in
     4.1 --- a/src/Pure/pattern.ML	Mon Dec 17 14:27:18 2001 +0100
     4.2 +++ b/src/Pure/pattern.ML	Tue Dec 18 02:17:20 2001 +0100
     4.3 @@ -183,7 +183,7 @@
     4.4  
     4.5  fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
     4.6    if T=U then env
     4.7 -  else let val (iTs',maxidx') = Type.unify (!tsgr) maxidx iTs (U,T)
     4.8 +  else let val (iTs',maxidx') = Type.unify (!tsgr) (iTs, maxidx) (U, T)
     4.9         in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
    4.10         handle Type.TUNIFY => raise Unif;
    4.11  
     5.1 --- a/src/Pure/unify.ML	Mon Dec 17 14:27:18 2001 +0100
     5.2 +++ b/src/Pure/unify.ML	Tue Dec 18 02:17:20 2001 +0100
     5.3 @@ -179,8 +179,7 @@
     5.4  
     5.5  fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
     5.6    if T=U then env
     5.7 -  else let val (iTs',maxidx') = Type.unify (#tsig(Sign.rep_sg (!sgr)))
     5.8 -                                                maxidx iTs (U,T)
     5.9 +  else let val (iTs',maxidx') = Type.unify (#tsig(Sign.rep_sg (!sgr))) (iTs, maxidx) (U, T)
    5.10         in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
    5.11         handle Type.TUNIFY => raise CANTUNIFY;
    5.12