src/Pure/Proof/proof_checker.ML

       let
         val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees prf Name.context;
 
         fun thm_of_atom thm Ts =
           let
-            val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
+            val tvars = rev (Term.add_tvars (Thm.full_prop_of thm) []);
             val (fmap, thm') = Thm.varifyT_global' [] thm;
             val ctye =
               (tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts);
           in
             Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))