--- 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