--- a/src/HOL/Tools/transfer.ML Thu Aug 22 17:13:46 2013 +0200
+++ b/src/HOL/Tools/transfer.ML Thu Aug 22 17:19:44 2013 +0200
@@ -16,6 +16,8 @@
val get_sym_relator_eq: Proof.context -> thm list
val get_relator_eq_raw: Proof.context -> thm list
val get_relator_domain: Proof.context -> thm list
+ val get_compound_lhs: Proof.context -> term Net.net
+ val get_compound_rhs: Proof.context -> term Net.net
val transfer_add: attribute
val transfer_del: attribute
val transferred_attribute: thm list -> attribute