diff -r 8b25e3b217bc -r 85efdadee8ae src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Tue Mar 30 12:47:39 2010 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Tue Mar 30 15:25:30 2010 +0200
@@ -179,7 +179,7 @@
           (PAxm ("Pure.reflexive", _, _) % _)) =
         let val (U, V) = (case T of
           Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
-        in SOME (prf %% (ax combination_axm [V, U] %> eq % ?? eq % ?? t % ?? t %%
+        in SOME (prf %% (ax combination_axm [U, V] %> eq % ?? eq % ?? t % ?? t %%
           (ax reflexive_axm [T] % ?? eq) %% (ax reflexive_axm [U] % ?? t)))
         end
 
@@ -229,7 +229,7 @@
           if member (op =) defs s then
             let
               val vs = vars_of prop;
-              val tvars = OldTerm.term_tvars prop;
+              val tvars = Term.add_tvars prop [] |> rev;
               val (_, rhs) = Logic.dest_equals prop;
               val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
                 (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),