# HG changeset patch
# User wenzelm
# Date 1683748887 -7200
# Node ID af3f1a4ba6e4212bf1e0c3f33b037c8b8e370d99
# Parent  51d135645d701f7cd37a240f8bc3cc0fbda5f8c8
proper Thm.trim_context / Thm.transfer;

diff -r 51d135645d70 -r af3f1a4ba6e4 src/HOL/Tools/SMT/z3_replay_rules.ML
--- a/src/HOL/Tools/SMT/z3_replay_rules.ML	Wed May 10 21:47:08 2023 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_rules.ML	Wed May 10 22:01:27 2023 +0200
@@ -26,7 +26,7 @@
 fun apply ctxt ct =
   let
     val net = Data.get (Context.Proof ctxt)
-    val xthms = Net.match_term net (Thm.term_of ct)
+    val xthms = map (Thm.transfer' ctxt) (Net.match_term net (Thm.term_of ct))
 
     fun select ct = map_filter (maybe_instantiate ct) xthms
     fun select' ct =
@@ -40,11 +40,12 @@
 fun ins thm net = Net.insert_term Thm.eq_thm (prep thm) net handle Net.INSERT => net
 fun del thm net = Net.delete_term Thm.eq_thm (prep thm) net handle Net.DELETE => net
 
-val add = Thm.declaration_attribute (Data.map o ins)
+val add = Thm.declaration_attribute (Data.map o ins o Thm.trim_context)
 val del = Thm.declaration_attribute (Data.map o del)
 
 val _ = Theory.setup
  (Attrib.setup \<^binding>\<open>z3_rule\<close> (Attrib.add_del add del) "declaration of Z3 proof rules" #>
-  Global_Theory.add_thms_dynamic (\<^binding>\<open>z3_rule\<close>, Net.content o Data.get))
+  Global_Theory.add_thms_dynamic (\<^binding>\<open>z3_rule\<close>,
+    fn context => map (Thm.transfer'' context) (Net.content (Data.get context))))
 
 end;