--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sun May 18 20:29:04 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon May 19 09:35:35 2014 +0200
@@ -195,8 +195,8 @@
fun mk_set_empty_tac ctxt ct exhaust sets discs =
TRYALL Goal.conjunction_tac THEN
ALLGOALS(rtac (Ctr_Sugar_Util.cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
- hyp_subst_tac ctxt) THEN
- Local_Defs.unfold_tac ctxt (sets @ map_filter (fn thm =>
+ REPEAT_DETERM o hyp_subst_tac ctxt) THEN
+ unfold_thms_tac ctxt (sets @ map_filter (fn thm =>
SOME (thm RS @{thm iffD2[OF eq_False]}) handle THM _ => NONE) discs) THEN
ALLGOALS(rtac refl ORELSE' etac FalseE);