src/Pure/Proof/proof_rewrite_rules.ML

       | rew' ((prf as PAxm ("Pure.combination", _, _) %
         SOME ((eq as Const ("==", T)) $ t) % _ % _ % _) %%
           (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
 
       | rew' _ = NONE;
   in rew' #> Option.map (rpair no_skel) end;

   | insert_refl defs Ts prf = (case strip_combt prf of
         (PThm (_, ((s, prop, SOME Ts), _)), ts) =>
           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),
                 map the ts);
             in