src/HOL/ex/atp_export.ML

 val ascii_of = ATP_Translate.ascii_of
 
 val fact_name_of = prefix ATP_Translate.fact_prefix o ascii_of
 
 fun facts_of thy =
-  Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty
+  Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) Symtab.empty
                                 true (K true) [] []
 
 fun fold_body_thms f =
   let
     fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>

     val names =
       [] |> fold_body_thms collect [Thm.proof_body_of thm] |> map fact_name_of
   in names end
 
 fun interesting_const_names ctxt =
-  let val thy = ProofContext.theory_of ctxt in
+  let val thy = Proof_Context.theory_of ctxt in
     Sledgehammer_Filter.const_names_in_fact thy
         (Sledgehammer_Provers.is_built_in_const_for_prover ctxt ATP_Systems.eN)
   end
 
 fun generate_tptp_graph_file_for_theory ctxt thy file_name =