author berghofe Thu, 19 Oct 2006 11:21:01 +0200 changeset 21054 6048c085c3ae parent 21053 7d0962594902 child 21055 e053811d680e
Split up FCBs into separate formulae for each binder.
```--- a/src/HOL/Nominal/nominal_package.ML	Wed Oct 18 23:15:16 2006 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Thu Oct 19 11:21:01 2006 +0200
@@ -1423,10 +1423,9 @@
HOLogic.mk_Trueprop (rec_set \$
list_comb (Const (cname, Ts ---> T), map Free frees) \$ result))],
rec_prems @ [list_all_free (frees @ frees'', Logic.list_implies (prems4, P))],
-         if null result_freshs then rec_prems'
-         else rec_prems' @ [list_all_free (frees @ frees'',
+         rec_prems' @ map (fn fr => list_all_free (frees @ frees'',
Logic.list_implies (List.nth (prems2, l) @ prems3 @ prems5 @ prems6 @ [P],
-             HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj result_freshs)))],
+             HOLogic.mk_Trueprop fr))) result_freshs,
rec_eq_prems @ [List.concat prems2 @ prems3],
l + 1)
end;
@@ -1648,7 +1647,7 @@
val k = length rec_fns;
val (finite_thss, ths1) = fold_map (fn T => fn xs =>
apfst (pair T) (chop k xs)) dt_atomTs prems;
-           val (P_ind_ths, ths2) = chop k ths1;
+           val (P_ind_ths, fcbs) = chop k ths1;
val P_ths = map (fn th => th RS mp) (split_conj_thm
(Goal.prove context
(map fst (rec_unique_frees'' @ rec_unique_frees')) []
@@ -1662,7 +1661,6 @@
val rec_fin_supp_thms' = map
(fn (ths, (T, fin_ths)) => (T, map (curry op MRS fin_ths) ths))
(rec_fin_supp_thms ~~ finite_thss);
-           val fcbs = List.concat (map split_conj_thm ths2);
in EVERY
([rtac induct_aux_rec 1] @
maps (fn (_, finite_ths) =>```