src/Pure/Proof/proof_checker.ML

 
 fun thm_of_proof thy =
   let val lookup = lookup_thm thy in
     fn prf =>
       let
-        val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
+        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 (fmap, thm') = Thm.varifyT_global' [] thm;