# HG changeset patch
# User wenzelm
# Date 1703446522 -3600
# Node ID e9828380e7e3c24bce241ac44e8eead20fef70e5
# Parent  fe4bd39bfeacf841dd08c18888795f8ef3866d4c
more robust: avoid crash of AFP/Transition_Systems_and_Automata (amending fe4bd39bfeac and 43d8385db923);

diff -r fe4bd39bfeac -r e9828380e7e3 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun Dec 24 20:17:08 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML	Sun Dec 24 20:35:22 2023 +0100
@@ -296,10 +296,10 @@
 
 local
 
-fun thm_def (name, pos) thm thy =
+fun thm_def (name, pos) thm lthy =
   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);
+    Local_Theory.background_theory_result (Thm.store_zproof ((name, 0), pos) thm) lthy  (* FIXME proper Thm_Name.T *)
+  else (thm, lthy);
 
 fun thm_definition (name, thm0) lthy =
   let
@@ -324,8 +324,7 @@
 
     (*thm definition*)
     val (global_thm, lthy') =
-      (Local_Theory.background_theory_result o thm_def name)
-        (Global_Theory.name_thm Global_Theory.official1 name schematic_thm) lthy;
+      thm_def name (Global_Theory.name_thm Global_Theory.official1 name schematic_thm) lthy;
 
     (*import fixes*)
     val (tvars, vars) =