diff -r ba80154a1118 -r 74b879546c33 src/HOL/Tools/transfer.ML
--- 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