--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Jan 11 11:56:35 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Jan 11 13:15:14 2016 +0100
@@ -156,6 +156,7 @@
val mk_tuple_balanced: term list -> term
val mk_tuple1_balanced: typ list -> term list -> term
val abs_curried_balanced: typ list -> term -> term
+ val mk_tupled_fun: term -> term -> term list -> term
val mk_case_sum: term * term -> term
val mk_case_sumN: term list -> term
@@ -461,8 +462,8 @@
if xs = [x] then f else HOLogic.tupled_lambda x (Term.list_comb (f, xs));
fun mk_case_absumprod absT rep fs xss xss' =
- HOLogic.mk_comp (mk_case_sumN_balanced (@{map 3} mk_tupled_fun fs (map mk_tuple_balanced xss) xss'),
- mk_rep absT rep);
+ HOLogic.mk_comp (mk_case_sumN_balanced
+ (@{map 3} mk_tupled_fun fs (map mk_tuple_balanced xss) xss'), mk_rep absT rep);
fun If_const T = Const (@{const_name If}, HOLogic.boolT --> T --> T --> T);
fun mk_If p t f = let val T = fastype_of t in If_const T $ p $ t $ f end;
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Jan 11 11:56:35 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Jan 11 13:15:14 2016 +0100
@@ -37,8 +37,6 @@
fun mk_abs_zero_nat T = Term.absdummy T HOLogic.zero;
-fun mk_pointful ctxt thm = unfold_thms ctxt [o_apply] (thm RS fun_cong);
-
fun mk_unabs_def_unused_0 n =
funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong);
--- a/src/HOL/Tools/BNF/bnf_util.ML Mon Jan 11 11:56:35 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML Mon Jan 11 13:15:14 2016 +0100
@@ -86,6 +86,7 @@
val mk_nthI: int -> int -> thm
val mk_nth_conv: int -> int -> thm
val mk_ordLeq_csum: int -> int -> thm -> thm
+ val mk_pointful: Proof.context -> thm -> thm
val mk_rel_funDN: int -> thm -> thm
val mk_rel_funDN_rotated: int -> thm -> thm
val mk_sym: thm -> thm
@@ -360,7 +361,6 @@
fun mk_trans thm1 thm2 = trans OF [thm1, thm2];
fun mk_sym thm = thm RS sym;
-(*TODO: antiquote heavily used theorems once*)
val prod_injectD = @{thm iffD1[OF prod.inject]};
val prod_injectI = @{thm iffD2[OF prod.inject]};
val ctrans = @{thm ordLeq_transitive};
@@ -374,6 +374,8 @@
val set_rev_mp = @{thm set_rev_mp};
val subset_UNIV = @{thm subset_UNIV};
+fun mk_pointful ctxt thm = unfold_thms ctxt [o_apply] (thm RS fun_cong);
+
fun mk_nthN 1 t 1 = t
| mk_nthN _ t 1 = HOLogic.mk_fst t
| mk_nthN 2 t 2 = HOLogic.mk_snd t