src/Provers/preorder.ML

 (* trans_tac - solves transitivity chains over <= *)
 
 fun trans_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
  let
   val thy = Proof_Context.theory_of ctxt;
-  val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
+  val rfrees = map Free (rev (Term.variant_frees A (Logic.strip_params A)));
   val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
   val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
   val lesss = flat (map_index (mkasm_trans thy o swap) Hs);
   val prfs = solveLeTrans thy (lesss, C);
 

 (* quasi_tac - solves quasi orders *)
 
 fun quasi_tac ctxt = SUBGOAL (fn (A, n) => fn st =>
  let
   val thy = Proof_Context.theory_of ctxt
-  val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
+  val rfrees = map Free (rev (Term.variant_frees A (Logic.strip_params A)));
   val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
   val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
   val lesss = flat (map_index (mkasm_quasi thy o swap) Hs);
   val prfs = solveQuasiOrder thy (lesss, C);
   val (subgoals, prf) = mkconcl_quasi thy C;