# HG changeset patch
# User blanchet
# Date 1428410300 -7200
# Node ID cfbaee8cdf1d4c4d4ec02d99c65a2459bb63a92a
# Parent  83071f4c8ae6dc197b61a43adf50551ae00e485d
export ML function

diff -r 83071f4c8ae6 -r cfbaee8cdf1d src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Apr 07 11:25:54 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Apr 07 14:38:20 2015 +0200
@@ -44,6 +44,8 @@
      fp_nesting_map_comps: thm list,
      ctr_specs: corec_ctr_spec list}
 
+  val abs_tuple_balanced: term list -> term -> term
+
   val fold_rev_let_if_case: Proof.context -> (term list -> term -> 'a -> 'a) -> typ list ->
     term -> 'a -> 'a
   val massage_let_if_case: Proof.context -> (term -> bool) -> (typ list -> term -> term) ->
@@ -158,6 +160,8 @@
 
 exception NO_MAP of term;
 
+val abs_tuple_balanced = HOLogic.tupled_lambda o mk_tuple_balanced;
+
 fun sort_list_duplicates xs = map snd (sort (int_ord o apply2 fst) xs);
 
 val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
@@ -562,8 +566,6 @@
 
 val undef_const = Const (@{const_name undefined}, dummyT);
 
-val abs_tuple_balanced = HOLogic.tupled_lambda o mk_tuple_balanced;
-
 fun abstract vs =
   let
     fun abs n (t $ u) = abs n t $ abs n u