Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Proof/proof_syntax.ML
changeset 80306 c2537860ccf8
parent 80295 8a9588ffc133 
--- 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
isabelle