# HG changeset patch
# User kuncar
# Date 1377184784 -7200
# Node ID 74b879546c33de39f62ead52308465afc7bb9f55
# Parent  ba80154a1118b9d7d20634d439d387ac6b794701
publish a private function

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