# HG changeset patch
# User desharna
# Date 1400484935 -7200
# Node ID 299b026cc5af80dd8dc96e4d6c7a6ad81dc2c6f9
# Parent  fafcf43ded4aec6b60d3e835a54fbea238c92a87
fix 'set_empty' theorem when the discriminator is 'op ='

diff -r fafcf43ded4a -r 299b026cc5af src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- 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);