merged
authorpaulson
Wed Sep 23 11:06:32 2009 +0100 (2009-09-23)
changeset 32649442e03154ee6
parent 32647 e54f47f9e28b
parent 32648 143e0b0a6b33
child 32650 34bfa2492298
child 32707 836ec9d0a0c8
merged
     1.1 --- a/src/Pure/envir.ML	Wed Sep 23 11:33:52 2009 +0200
     1.2 +++ b/src/Pure/envir.ML	Wed Sep 23 11:06:32 2009 +0100
     1.3 @@ -282,12 +282,9 @@
     1.4    let
     1.5      val funerr = "fastype: expected function type";
     1.6      fun fast Ts (f $ u) =
     1.7 -          (case fast Ts f of
     1.8 +          (case Type.devar tyenv (fast Ts f) of
     1.9              Type ("fun", [_, T]) => T
    1.10 -          | TVar v =>
    1.11 -              (case Type.lookup tyenv v of
    1.12 -                SOME (Type ("fun", [_, T])) => T
    1.13 -              | _ => raise TERM (funerr, [f $ u]))
    1.14 +          | TVar v => raise TERM (funerr, [f $ u])
    1.15            | _ => raise TERM (funerr, [f $ u]))
    1.16        | fast Ts (Const (_, T)) = T
    1.17        | fast Ts (Free (_, T)) = T
     2.1 --- a/src/Pure/type.ML	Wed Sep 23 11:33:52 2009 +0200
     2.2 +++ b/src/Pure/type.ML	Wed Sep 23 11:06:32 2009 +0100
     2.3 @@ -55,6 +55,7 @@
     2.4    exception TYPE_MATCH
     2.5    type tyenv = (sort * typ) Vartab.table
     2.6    val lookup: tyenv -> indexname * sort -> typ option
     2.7 +  val devar: tyenv -> typ -> typ
     2.8    val typ_match: tsig -> typ * typ -> tyenv -> tyenv
     2.9    val typ_instance: tsig -> typ * typ -> bool
    2.10    val raw_match: typ * typ -> tyenv -> tyenv