src/HOL/Tools/Sledgehammer/sledgehammer_util.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Oct 24 22:05:57 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Oct 25 15:31:58 2024 +0200
@@ -115,14 +115,12 @@
 
 fun thms_of_name ctxt name =
   let
-    val get = maps (Proof_Context.get_fact ctxt o fst)
     val keywords = Thy_Header.get_keywords' ctxt
   in
-    Symbol_Pos.explode (name, Position.start)
-    |> Token.tokenize keywords {strict = false}
+    Token.explode keywords Position.start name
     |> filter Token.is_proper
     |> Source.of_list
-    |> Source.source Token.stopper (Parse.thms1 >> get)
+    |> Source.source' (Context.Proof ctxt) Token.stopper Attrib.multi_thm
     |> Source.exhaust
   end