# HG changeset patch
# User blanchet
# Date 1409777225 -7200
# Node ID d84bab7ed89e2dfeb11bb369be2743140fda95dd
# Parent  68a2cf857df1f65142839a8922f2c585c589ce41
fixed tactic for n-way mutual recursion, n >= 4 (balanced conjunctions confuse the tactic)

diff -r 68a2cf857df1 -r d84bab7ed89e src/HOL/Library/bnf_lfp_countable.ML
--- a/src/HOL/Library/bnf_lfp_countable.ML	Wed Sep 03 22:47:05 2014 +0200
+++ b/src/HOL/Library/bnf_lfp_countable.ML	Wed Sep 03 22:47:05 2014 +0200
@@ -160,7 +160,7 @@
       val (xs, names_ctxt) = ctxt |> mk_Frees "x" fpTs;
 
       val conjuncts = map3 mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0);
-      val goal = HOLogic.mk_Trueprop (Balanced_Tree.make HOLogic.mk_conj conjuncts);
+      val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj conjuncts);
     in
       Goal.prove ctxt [] [] goal (fn {context = ctxt, prems = _} =>
         mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps'