# HG changeset patch
# User berghofe
# Date 1161249661 -7200
# Node ID 6048c085c3ae2a133e66406b2e42b9e148d9c698
# Parent  7d09625949021c64ebae98b978a1e57d601381db
Split up FCBs into separate formulae for each binder.

diff -r 7d0962594902 -r 6048c085c3ae src/HOL/Nominal/nominal_package.ML
--- 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) =>