# HG changeset patch
# User paulson
# Date 1253700392 -3600
# Node ID 442e03154ee6f4d857cf5a57a140094086feab18
# Parent  e54f47f9e28b2d166da8609a0b714c7101441d3e# Parent  143e0b0a6b33210d2f8ed52fab9be5e80be660b2
merged

diff -r e54f47f9e28b -r 442e03154ee6 src/Pure/envir.ML
--- 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
diff -r e54f47f9e28b -r 442e03154ee6 src/Pure/type.ML
--- 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