# HG changeset patch
# User blanchet
# Date 1380045280 -7200
# Node ID 34c51a1d2555d5411437aaa85f20923162f14b6e
# Parent  ff09afd47b34d542090b7a62100468b2ae350c3e
temporary fix to tactic

diff -r ff09afd47b34 -r 34c51a1d2555 src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Tue Sep 24 19:15:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Tue Sep 24 19:54:40 2013 +0200
@@ -78,7 +78,8 @@
   HEADGOAL (REPEAT o rtac @{thm eq_ifI}) THEN
   mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
   REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt) THEN
-  HEADGOAL (asm_simp_tac (ss_only @{thms if_True if_False not_False_eq_True} ctxt));
+  (* FIXME: Something like (ss_only @{thms if_True if_False not_False_eq_True simp_thms} ctxt) *)
+  HEADGOAL (asm_simp_tac ctxt);
 
 fun mk_primcorec_code_of_ctr_tac ctxt ms ctr_thms =
   EVERY (map2 (mk_primcorec_code_of_ctr_case_tac ctxt) ms ctr_thms);