# HG changeset patch
# User blanchet
# Date 1347654191 -7200
# Node ID 83b867707af2b135b1e66f54a956d76cd56d0494
# Parent  94ad5ba23541bfeba54ea351434ec68a42539c74
merged two unfold steps

diff -r 94ad5ba23541 -r 83b867707af2 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 22:23:11 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 22:23:11 2012 +0200
@@ -123,8 +123,8 @@
 fun mk_induct_discharge_prem_prems_tac ctxt nn ixs set_natural's pre_set_defs =
   EVERY' (maps (fn ((pp, jj), (qq, kk)) =>
       [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
-       SELECT_GOAL (Local_Defs.unfold_tac ctxt pre_set_defs), (* FIXME: ### why on a line of its own? *)
-       SELECT_GOAL (Local_Defs.unfold_tac ctxt (set_natural's @ induct_prem_prem_thms)),
+       SELECT_GOAL (Local_Defs.unfold_tac ctxt
+         (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
        SELECT_GOAL (Local_Defs.unfold_tac ctxt
          (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
        rtac (mk_UnIN pp jj) THEN' mk_induct_prem_prem_endgame_tac ctxt qq ORELSE'