# HG changeset patch
# User desharna
# Date 1405498285 -7200
# Node ID c1238062184bd7cb955ff7c55049d3886a8c9a6c
# Parent  8200e1eb367f746a63fc09cfc201452488541cbc
fix rel_cases

diff -r 8200e1eb367f -r c1238062184b src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jul 15 17:49:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Jul 16 10:11:25 2014 +0200
@@ -1390,7 +1390,7 @@
                 map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th)
                   rel_inject_thms ms;
 
-              val (disc_map_iff_thms, sel_map_thms, sel_set_thms (* FIXME: , (rel_cases_thm, rel_cases_attrs) *)) =
+              val (disc_map_iff_thms, sel_map_thms, sel_set_thms, (rel_cases_thm, rel_cases_attrs)) =
                 let
                   val (((Ds, As), Bs), names_lthy) = lthy
                     |> mk_TFrees (dead_of_bnf fp_bnf)
@@ -1407,7 +1407,6 @@
                   val selssA = map (map (mk_disc_or_sel ADs)) selss;
                   val disc_sel_pairs = flat (map2 (map o pair) discsA selssA);
 
-(* FIXME:
                   val (rel_cases_thm, rel_cases_attrs) =
                     let
                       val rel = mk_rel_of_bnf Ds As Bs fp_bnf;
@@ -1461,7 +1460,6 @@
                     in
                       (thm, [consumes_attr, case_names_attr, cases_pred_attr ""])
                     end;
-*)
 
                   val disc_map_iff_thms =
                     let
@@ -1585,7 +1583,7 @@
                           |> Proof_Context.export names_lthy lthy
                     end;
                 in
-                  (disc_map_iff_thms, sel_map_thms, sel_set_thms (* FIXME: , (rel_cases_thm, rel_cases_attrs) *))
+                  (disc_map_iff_thms, sel_map_thms, sel_set_thms, (rel_cases_thm, rel_cases_attrs))
                 end;
 
               val anonymous_notes =
@@ -1596,7 +1594,7 @@
               val notes =
                 [(disc_map_iffN, disc_map_iff_thms, simp_attrs),
                  (mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs),
-(* FIXME:                 (rel_casesN, [rel_cases_thm], rel_cases_attrs), *)
+                 (rel_casesN, [rel_cases_thm], rel_cases_attrs),
                  (rel_distinctN, rel_distinct_thms, simp_attrs),
                  (rel_injectN, rel_inject_thms, simp_attrs),
                  (rel_introsN, rel_intro_thms, []),
diff -r 8200e1eb367f -r c1238062184b src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Jul 15 17:49:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Jul 16 10:11:25 2014 +0200
@@ -221,8 +221,11 @@
     True_implies_equals conj_imp_eq_imp_imp} @
     map (fn thm => thm RS eqFalseI) (distincts @ rel_distincts) @
     map (fn thm => thm RS eqTrueI) rel_injects) THEN
-  TRYALL (atac ORELSE' etac FalseE ORELSE' (REPEAT_DETERM o dtac @{thm meta_spec} THEN'
-    REPEAT_DETERM o (dtac @{thm meta_mp} THEN' rtac refl) THEN' Goal.assume_rule_tac ctxt));
+  TRYALL (atac ORELSE' etac FalseE ORELSE'
+    (REPEAT_DETERM o dtac @{thm meta_spec} THEN'
+     TRY o filter_prems_tac
+       (forall (curry (op <>) (HOLogic.mk_Trueprop @{term False})) o Logic.strip_imp_prems) THEN'
+     REPEAT_DETERM o (dtac @{thm meta_mp} THEN' rtac refl) THEN' Goal.assume_rule_tac ctxt));
 
 fun mk_rel_coinduct0_tac ctxt dtor_rel_coinduct cts assms exhausts discss selss ctor_defss
     dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses nesting_rel_eqs =