From 95b30e8b5f4579c9027ed3d9e5623e4e9f4e63a8 Mon Sep 17 00:00:00 2001
From: "Achim D. Brucker" <adbrucker@0x5f.org>
Date: Thu, 13 Mar 2025 14:45:00 +0000
Subject: [PATCH] Update to latest development version of Isabelle.

---
 Isabelle_DOF-Proofs/Reification_Test.thy       | 18 +++++++++---------
 .../Very_Deep_Interpretation.thy               |  4 ++--
 2 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/Isabelle_DOF-Proofs/Reification_Test.thy b/Isabelle_DOF-Proofs/Reification_Test.thy
index 768748e..faab56d 100644
--- a/Isabelle_DOF-Proofs/Reification_Test.thy
+++ b/Isabelle_DOF-Proofs/Reification_Test.thy
@@ -403,7 +403,7 @@ ML\<open>
   (*all theorems used in the graph of nested proofs*)
   val all_thms =
     Proofterm.fold_body_thms
-      (fn {name, ...} => insert (op =) name) [body] [];
+      (fn {thm_name, ...} => insert (op =) thm_name) [body] [];
 \<close>
 
 term*\<open>@{thm \<open>Reification_Test.identity_conc\<close>}\<close>
@@ -434,7 +434,7 @@ ML\<open>
   (*all theorems used in the graph of nested proofs*)
   val all_thms =
     Proofterm.fold_body_thms
-      (fn {name, ...} => insert (op =) name) [body] [];
+      (fn {thm_name, ...} => insert (op =) thm_name) [body] [];
 \<close>
 
 declare[[show_sorts = false]]
@@ -458,7 +458,7 @@ ML\<open>
   (*all theorems used in the graph of nested proofs*)
   val all_thms =
     Proofterm.fold_body_thms
-      (fn {name, ...} => insert (op =) name) [body] [];
+      (fn {thm_name, ...} => insert (op =) thm_name) [body] [];
 \<close>
 
 prf test
@@ -485,7 +485,7 @@ ML\<open>
   (*all theorems used in the graph of nested proofs*)
   val all_thms =
     Proofterm.fold_body_thms
-      (fn {name, ...} => insert (op =) name) [body] [];
+      (fn {thm_name, ...} => insert (op =) thm_name) [body] [];
 \<close>
 
 prf test2
@@ -510,7 +510,7 @@ ML\<open>
   (*all theorems used in the graph of nested proofs*)
   val all_thms =
     Proofterm.fold_body_thms
-      (fn {name, ...} => insert (op =) name) [body] [];
+      (fn {thm_name, ...} => insert (op =) thm_name) [body] [];
 \<close>
 
 prf test3
@@ -535,7 +535,7 @@ ML\<open>
   (*all theorems used in the graph of nested proofs*)
   val all_thms =
     Proofterm.fold_body_thms
-      (fn {name, ...} => insert (op =) name) [body] [];
+      (fn {thm_name, ...} => insert (op =) thm_name) [body] [];
 \<close>
 
 prf test4
@@ -560,7 +560,7 @@ ML\<open>
   (*all theorems used in the graph of nested proofs*)
   val all_thms =
     Proofterm.fold_body_thms
-      (fn {name, ...} => insert (op =) name) [body] [];
+      (fn {thm_name, ...} => insert (op =) thm_name) [body] [];
 \<close>
 
 prf symmetric
@@ -635,7 +635,7 @@ ML\<open>
   (*all theorems used in the graph of nested proofs*)
   val all_thms =
     Proofterm.fold_body_thms
-      (fn {name, ...} => insert (op =) name) [body] [];
+      (fn {thm_name, ...} => insert (op =) thm_name) [body] [];
 \<close>
 ML\<open>
 val thy = \<^theory>;
@@ -700,7 +700,7 @@ ML\<open>
   (*all theorems used in the graph of nested proofs*)
   val all_thms =
     Proofterm.fold_body_thms
-      (fn {name, ...} => insert (op =) name) [body] [];
+      (fn {thm_name, ...} => insert (op =) thm_name) [body] [];
 \<close>
 
 ML\<open>
diff --git a/Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy b/Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy
index 0361e9b..22bb35b 100644
--- a/Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy
+++ b/Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy
@@ -162,12 +162,12 @@ fun ML_isa_elaborate_thms_of (thy:theory) _ _ term_option pos =
           val thm_name = HOLogic.dest_string term
           val thm = Proof_Context.get_thm (Proof_Context.init_global thy) thm_name
           val body = Proofterm.strip_thm_body (Thm.proof_body_of thm)
-          val all_thms_name = Proofterm.fold_body_thms (fn {name, ...} => insert (op =) name) [body] []
+          val all_thms_name = Proofterm.fold_body_thms (fn {thm_name, ...} => insert (op =) thm_name) [body] []
           (*val all_thms = map (Proof_Context.get_thm (Proof_Context.init_global thy)) all_thms_name*)
           (*val all_proofs = map (Proof_Syntax.standard_proof_of
                                    {full = true, expand_name = Thm.expand_name thm}) all_thms*)
         (*in HOLogic.mk_list \<^Type>\<open>thm\<close> (map (fn proof => \<^Const>\<open>Thm_content\<close> $ reify_proofterm proof) all_proofs) end*)
-        in HOLogic.mk_list \<^typ>\<open>string\<close> (map HOLogic.mk_string all_thms_name) end
+        in HOLogic.mk_list \<^typ>\<open>string\<close> (map HOLogic.mk_string (map (Proof_Context.print_thm_name (Proof_Context.init_global thy)) all_thms_name)) end
 
 fun ML_isa_elaborate_trace_attribute (thy:theory) _ _ term_option pos =
 case term_option of