# HG changeset patch
# User paulson
# Date 1253700328 -3600
# Node ID 143e0b0a6b33210d2f8ed52fab9be5e80be660b2
# Parent  1e2872252f913ef37281435a82cb2fdcf2128d50
Correct chasing of type variable instantiations during type unification.
The following theory should not raise exception TERM:

constdefs
 somepredicate :: "(('b => 'b) => ('a => 'a))
                             => 'a => 'b => bool"
"somepredicate upd v x == True"

lemma somepredicate_idI:
 "somepredicate id (f v) v"
 by (simp add: somepredicate_def)

lemma somepredicate_triv:
 "somepredicate upd v x ==> somepredicate upd v x"
 by assumption

lemmas somepredicate_triv [OF somepredicate_idI]

lemmas st' = somepredicate_triv[where v="h :: nat => bool"]

lemmas st2 = st'[OF somepredicate_idI]

diff -r 1e2872252f91 -r 143e0b0a6b33 src/Pure/envir.ML
--- a/src/Pure/envir.ML	Thu Sep 17 15:04:46 2009 +0100
+++ b/src/Pure/envir.ML	Wed Sep 23 11:05:28 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 1e2872252f91 -r 143e0b0a6b33 src/Pure/type.ML
--- a/src/Pure/type.ML	Thu Sep 17 15:04:46 2009 +0100
+++ b/src/Pure/type.ML	Wed Sep 23 11:05:28 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