# HG changeset patch
# User wenzelm
# Date 1703591170 -3600
# Node ID 5b01b93de0627011fcf9584f4fc8257cce8bf646
# Parent  b191339a014c4fa58dd3b6c5619f2f4612007201
more robust: avoid crash of Thm.solve_constraints due to changed background theory, e.g. relevant for AFP/Transition_Systems_and_Automata;

diff -r b191339a014c -r 5b01b93de062 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Tue Dec 26 12:37:33 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML	Tue Dec 26 12:46:10 2023 +0100
@@ -306,12 +306,11 @@
     Local_Theory.background_theory_result (Thm.store_zproof (name, pos) thm) lthy
   else (thm, lthy);
 
-fun thm_definition (name_pos, thm0) lthy =
+fun thm_definition (name_pos, thm) lthy =
   let
     val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
 
     (*export assumes/defines*)
-    val thm = Goal.norm_result lthy thm0;
     val ((defs, asms), thm') = Local_Defs.export lthy thy_ctxt thm;
     val asms' = map (rewrite_rule lthy (Drule.norm_hhf_eqs @ defs)) asms;
 
@@ -361,8 +360,9 @@
 
 in
 
-fun notes target_notes kind facts lthy =
+fun notes target_notes kind facts0 lthy =
   let
+    val facts = Attrib.map_thms (Goal.norm_result lthy) facts0;
     val (facts', lthy') =
       (facts, lthy) |-> fold_map (fn (a, thms) => fn lthy1 =>
         let