--- 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;