# HG changeset patch
# User wenzelm
# Date 1702850240 -3600
# Node ID fb8ed7fbb537313bad3b9a99ff5df5bef2f36ac2
# Parent  d1e5f6d1ddca128b08c0e3ccbc96307bb1fa14cb
proper Thm.transfer (required for zproofs);

diff -r d1e5f6d1ddca -r fb8ed7fbb537 src/HOL/Tools/Transfer/transfer.ML
--- a/src/HOL/Tools/Transfer/transfer.ML	Sun Dec 17 21:43:14 2023 +0100
+++ b/src/HOL/Tools/Transfer/transfer.ML	Sun Dec 17 22:57:20 2023 +0100
@@ -385,7 +385,7 @@
 (** Adding transfer domain rules **)
 
 fun prep_transfer_domain_thm ctxt =
-  abstract_equalities_domain ctxt o detect_transfer_rules
+  abstract_equalities_domain ctxt o detect_transfer_rules o Thm.transfer' ctxt
 
 fun add_transfer_domain_thm thm ctxt =
   (add_transfer_thm o prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt