src/Pure/pattern.ML
changeset 32032 a6a6e8031c14
parent 30565 784be11cb70e
child 32035 8e77b6a250d5
     1.1 --- a/src/Pure/pattern.ML	Fri Jul 17 21:33:00 2009 +0200
     1.2 +++ b/src/Pure/pattern.ML	Fri Jul 17 21:33:00 2009 +0200
     1.3 @@ -141,8 +141,10 @@
     1.4    | split_type (Type ("fun",[T1,T2]),n,Ts) = split_type (T2,n-1,T1::Ts)
     1.5    | split_type _                           = error("split_type");
     1.6  
     1.7 -fun type_of_G (env as Envir.Envir {iTs, ...}) (T,n,is) =
     1.8 -  let val (Ts, U) = split_type (Envir.norm_type iTs T, n, [])
     1.9 +fun type_of_G env (T, n, is) =
    1.10 +  let
    1.11 +    val tyenv = Envir.type_env env;
    1.12 +    val (Ts, U) = split_type (Envir.norm_type tyenv T, n, []);
    1.13    in map (nth Ts) is ---> U end;
    1.14  
    1.15  fun mkhnf (binders,is,G,js) = mkabs (binders, is, app(G,js));
    1.16 @@ -225,11 +227,12 @@
    1.17                   end;
    1.18    in if TermOrd.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
    1.19  
    1.20 -fun unify_types thy (T,U) (env as Envir.Envir{asol,iTs,maxidx}) =
    1.21 -  if T=U then env
    1.22 -  else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx)
    1.23 -       in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
    1.24 -       handle Type.TUNIFY => (typ_clash thy (iTs,T,U); raise Unif);
    1.25 +fun unify_types thy (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) =
    1.26 +  if T = U then env
    1.27 +  else
    1.28 +    let val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx)
    1.29 +    in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end
    1.30 +    handle Type.TUNIFY => (typ_clash thy (tyenv, T, U); raise Unif);
    1.31  
    1.32  fun unif thy binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of
    1.33        (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>