# HG changeset patch
# User wenzelm
# Date 1135347404 -3600
# Node ID ef36f9be255edb08f40326e73015937a56d4ada9
# Parent  1b96c86711627916aa8860d497142f1b4e30cd6a
proper treatment of nested conjunctions, i.e. simultaneous goals and mutual rules;

diff -r 1b96c8671162 -r ef36f9be255e src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Fri Dec 23 14:33:28 2005 +0100
+++ b/src/Provers/induct_method.ML	Fri Dec 23 15:16:44 2005 +0100
@@ -417,8 +417,8 @@
       ruleq
       |> Seq.maps (RuleCases.consume (List.concat defs) facts)
       |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
-        (CONJUNCTS (length concls) (ALLGOALS (fn j =>
-          (CONJUNCTS ~1 (ALLGOALS
+        (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
+          (CONJUNCTS (ALLGOALS
             (Method.insert_tac (more_facts @ nth_list atomized_defs (j - 1))
               THEN' fix_tac defs_ctxt
                 (nth concls (j - 1) + more_consumes)