# HG changeset patch
# User wenzelm
# Date 1703445428 -3600
# Node ID fe4bd39bfeacf841dd08c18888795f8ef3866d4c
# Parent  43d8385db923774773d19d5b0d3eb53ddbebec5d
more robust: zproofs need to be enabled (amending 43d8385db923);

diff -r 43d8385db923 -r fe4bd39bfeac src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun Dec 24 13:58:25 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML	Sun Dec 24 20:17:08 2023 +0100
@@ -296,6 +296,11 @@
 
 local
 
+fun thm_def (name, pos) thm thy =
+  if name <> "" andalso Proofterm.zproof_enabled (Proofterm.get_proofs_level ()) then
+    Thm.store_zproof ((name, 0), pos) thm thy  (* FIXME proper Thm_Name.T *)
+  else (thm, thy);
+
 fun thm_definition (name, thm0) lthy =
   let
     val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
@@ -319,7 +324,7 @@
 
     (*thm definition*)
     val (global_thm, lthy') =
-      (Local_Theory.background_theory_result o yield_singleton (Global_Theory.register_proofs name))
+      (Local_Theory.background_theory_result o thm_def name)
         (Global_Theory.name_thm Global_Theory.official1 name schematic_thm) lthy;
 
     (*import fixes*)