--- a/src/Pure/envir.ML Wed Sep 23 11:33:52 2009 +0200
+++ b/src/Pure/envir.ML Wed Sep 23 11:06:32 2009 +0100
@@ -282,12 +282,9 @@
let
val funerr = "fastype: expected function type";
fun fast Ts (f $ u) =
- (case fast Ts f of
+ (case Type.devar tyenv (fast Ts f) of
Type ("fun", [_, T]) => T
- | TVar v =>
- (case Type.lookup tyenv v of
- SOME (Type ("fun", [_, T])) => T
- | _ => raise TERM (funerr, [f $ u]))
+ | TVar v => raise TERM (funerr, [f $ u])
| _ => raise TERM (funerr, [f $ u]))
| fast Ts (Const (_, T)) = T
| fast Ts (Free (_, T)) = T
--- a/src/Pure/type.ML Wed Sep 23 11:33:52 2009 +0200
+++ b/src/Pure/type.ML Wed Sep 23 11:06:32 2009 +0100
@@ -55,6 +55,7 @@
exception TYPE_MATCH
type tyenv = (sort * typ) Vartab.table
val lookup: tyenv -> indexname * sort -> typ option
+ val devar: tyenv -> typ -> typ
val typ_match: tsig -> typ * typ -> tyenv -> tyenv
val typ_instance: tsig -> typ * typ -> bool
val raw_match: typ * typ -> tyenv -> tyenv