src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

   handle ERROR msg => ("error: " ^ msg, SH_ERROR)
 
 fun thms_of_name ctxt name =
   let
     val lex = Keyword.get_lexicons
-    val get = maps (ProofContext.get_fact ctxt o fst)
+    val get = maps (Proof_Context.get_fact ctxt o fst)
   in
     Source.of_string name
     |> Symbol.source
     |> Token.source {do_recover=SOME false} lex Position.start
     |> Token.source_proper