diff -r 95b51df1382e -r c2537860ccf8 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Sun Jun 09 15:11:07 2024 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Sun Jun 09 15:31:33 2024 +0200
@@ -143,7 +143,7 @@
 
 fun proof_of_term thy ty =
   let
-    val thms = Global_Theory.all_thms_of thy true;
+    val thms = Global_Theory.all_thms_of thy true |> map (apfst Thm_Name.short);
     val axms = Theory.all_axioms_of thy;
 
     fun mk_term t = (if ty then I else map_types (K dummyT))
@@ -200,7 +200,8 @@
 
 fun read_term thy topsort =
   let
-    val thm_names = filter_out (fn s => s = "") (map fst (Global_Theory.all_thms_of thy true));
+    val thm_names =
+      filter_out (fn s => s = "") (map (Thm_Name.short o fst) (Global_Theory.all_thms_of thy true));
     val axm_names = map fst (Theory.all_axioms_of thy);
     val ctxt = thy
       |> add_proof_syntax