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_checker.ML
changeset 81534 c32ebdcbe8ca
parent 81505 01f2936ec85e 
--- a/src/Pure/Proof/proof_checker.ML	Mon Dec 02 11:08:36 2024 +0100
+++ b/src/Pure/Proof/proof_checker.ML	Mon Dec 02 11:22:44 2024 +0100
@@ -72,7 +72,10 @@
   end;
 
 fun thm_of_proof thy =
-  let val lookup = lookup_thm thy in
+  let
+    val global_ctxt = Syntax.init_pretty_global thy;
+    val lookup = lookup_thm thy;
+  in
     fn prf =>
       let
         val prf_names =
@@ -96,9 +99,9 @@
                   if is_equal prop prop' then ()
                   else
                     error ("Duplicate use of theorem name " ^
-                      quote (Global_Theory.print_thm_name thy thm_name) ^ Position.here thm_pos
-                      ^ "\n" ^ Syntax.string_of_term_global thy prop
-                      ^ "\n\n" ^ Syntax.string_of_term_global thy prop');
+                      quote (Global_Theory.print_thm_name global_ctxt thm_name) ^ Position.here thm_pos
+                      ^ "\n" ^ Syntax.string_of_term global_ctxt prop
+                      ^ "\n\n" ^ Syntax.string_of_term global_ctxt prop');
               in thm_of_atom thm Ts end
 
           | thm_of _ _ (PAxm (name, _, SOME Ts)) =
isabelle