# HG changeset patch
# User blanchet
# Date 1347654191 -7200
# Node ID 7860bd1429f4b6e2e255be6af551bfea495a1a7a
# Parent  19237e4650553fd4eb4ccc090e09bf267f8b1660
provide more guidance, exploiting our knowledge of the goal

diff -r 19237e465055 -r 7860bd1429f4 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 22:23:10 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 22:23:11 2012 +0200
@@ -112,12 +112,12 @@
 val induct_prem_prem_thms_delayed =
   @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
 
-fun mk_induct_prem_prem_endgame_tac ctxt qq =
-  atac ORELSE'
-  rtac @{thm singletonI} ORELSE'
-  (REPEAT_DETERM o (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
-     etac @{thm induct_set_step}) THEN'
-   (atac ORELSE' blast_tac ctxt));
+fun mk_induct_prem_prem_endgame_tac _ 0 = atac ORELSE' rtac @{thm singletonI}
+  | mk_induct_prem_prem_endgame_tac ctxt qq =
+    REPEAT_DETERM_N qq o
+      (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
+       etac @{thm induct_set_step}) THEN'
+    (atac ORELSE' blast_tac ctxt);
 
 (* TODO: Get rid of the "blast_tac" *)
 fun mk_induct_discharge_prem_prems_tac ctxt nn ixs set_natural's pre_set_defs =