--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Tue Jul 09 21:13:14 2024 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Wed Jul 10 08:37:54 2024 +0200
@@ -103,9 +103,11 @@
let
fun split (s: string) : string * string =
- case first_field "(" s of
- NONE => (s,"")
- | SOME (name,isp) => (name, String.substring (isp, 0, size isp - 1))
+ if String.isPrefix "\<open>" s then (s,"")
+ else
+ case first_field "(" s of
+ NONE => (s,"")
+ | SOME (name,isp) => (name, String.substring (isp, 0, size isp - 1))
fun merge ((name1,is1) :: (name2,is2) :: zs) =
if name1 = name2