# HG changeset patch
# User nipkow
# Date 1720593474 -7200
# Node ID f86bcf439837292a6606ac2892d46dbaed8226f2
# Parent  34a5ca6fcdddf8f1962eae26371a429c3861d8c0
take care of facts in cartouches

diff -r 34a5ca6fcddd -r f86bcf439837 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- 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