src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

     ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
   let
     fun do_method named_thms ctxt =
       let
         val ref_of_str =
-          suffix ";" #> Outer_Syntax.scan Position.none #> Parse_Spec.xthm
+          suffix ";" #> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none #> Parse_Spec.xthm
           #> fst
         val thms = named_thms |> maps snd
         val facts = named_thms |> map (ref_of_str o fst o fst)
         val fact_override = {add = facts, del = [], only = true}
         fun my_timeout time_slice =

             ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms
         else if String.isPrefix "metis (" (!meth) then
           let
             val (type_encs, lam_trans) =
               !meth
-              |> Outer_Syntax.scan Position.start
+              |> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.start
               |> filter Token.is_proper |> tl
               |> Metis_Tactic.parse_metis_options |> fst
               |>> the_default [ATP_Proof_Reconstruct.partial_typesN]
               ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans
           in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end