# HG changeset patch
# User blanchet
# Date 1387615469 -3600
# Node ID 7f30d569da084dfa3b51e93574fde09bcdf31b69
# Parent  a020f7d74feda606a5f1dadb2eb24436cf140212
made tactic work with theorems with multiple assumptions

diff -r a020f7d74fed -r 7f30d569da08 src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Sat Dec 21 09:44:28 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Sat Dec 21 09:44:29 2013 +0100
@@ -126,7 +126,11 @@
         NONE => (ms, f_ctrs)
       | SOME nchotomy =>
         (ms |> split_last ||> K [n - 1] |> op @,
-         f_ctrs |> split_last ||> (fn thm => [rulify_nchotomy n nchotomy RS thm]) |> op @));
+         f_ctrs
+         |> split_last
+         ||> unfold_thms ctxt @{thms atomize_conjL}
+         ||> (fn thm => [rulify_nchotomy n nchotomy RS thm])
+         |> op @));
   in
     EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
       ms' f_ctrs') THEN