# HG changeset patch
# User kuncar
# Date 1379325297 -7200
# Node ID 96814d676c49c659f7c902e77ffa7332dafd4870
# Parent  9245797294037a634fe8f2d98a148212266be354
public access to the raw transfer rules - for restoring transferring

diff -r 924579729403 -r 96814d676c49 src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Mon Sep 16 11:22:06 2013 +0200
+++ b/src/HOL/Tools/transfer.ML	Mon Sep 16 11:54:57 2013 +0200
@@ -20,6 +20,8 @@
   val get_compound_rhs: Proof.context -> (term * thm) Item_Net.T
   val transfer_add: attribute
   val transfer_del: attribute
+  val transfer_raw_add: thm -> Context.generic -> Context.generic
+  val transfer_raw_del: thm -> Context.generic -> Context.generic
   val transferred_attribute: thm list -> attribute
   val untransferred_attribute: thm list -> attribute
   val transfer_domain_add: attribute
@@ -135,8 +137,6 @@
       | _ => I) o
    map_known_frees (Term.add_frees (Thm.concl_of thm)))
 
-fun get_args n = rev o fst o funpow_yield n (swap o dest_comb)
-
 fun del_transfer_thm thm = Data.map 
   (map_transfer_raw (Item_Net.remove thm) o
    map_compound_lhs
@@ -150,6 +150,9 @@
           Item_Net.remove (rhs, thm)
       | _ => I))
 
+fun transfer_raw_add thm ctxt = add_transfer_thm thm ctxt
+fun transfer_raw_del thm ctxt = del_transfer_thm thm ctxt
+
 (** Conversions **)
 
 fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}