src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML

      sel_defs: thm list,
      fp_nesting_maps: thm list,
      fp_nesting_map_ident0s: thm list,
      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) ->
     typ list -> term -> term

    fp_nesting_map_ident0s: thm list,
    fp_nesting_map_comps: thm list,
    ctr_specs: corec_ctr_spec list};
 
 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};
 val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};

      is_some gfp_sugar_thms, lthy)
   end;
 
 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
       | abs n (Abs (v, T, b)) = Abs (v, T, abs (n + 1) b)
       | abs n t =