# HG changeset patch
# User blanchet
# Date 1405377307 -7200
# Node ID 6bb3dd7f8097eadfe8b1ccc01d5e74150ac8f983
# Parent  242ce8d3d16b3a30b1e87faffa7475fe4e3c397e
took out 'rel_cases' for now because of failing tactic

diff -r 242ce8d3d16b -r 6bb3dd7f8097 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Jul 15 00:21:32 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Jul 15 00:35:07 2014 +0200
@@ -886,8 +886,9 @@
 @{thm list.rel_intros(1)[no_vars]} \\
 @{thm list.rel_intros(2)[no_vars]}
 
-\item[@{text "t."}\hthm{rel_cases} @{text "[consumes 1, case_names t\<^sub>1 \<dots> t\<^sub>m, cases pred]"}\rm:] ~ \\
-@{thm list.rel_cases[no_vars]}
+% FIXME (and add @ before antiquotation below)
+%\item[@{text "t."}\hthm{rel_cases} @{text "[consumes 1, case_names t\<^sub>1 \<dots> t\<^sub>m, cases pred]"}\rm:] ~ \\
+%{thm list.rel_cases[no_vars]}
 
 \end{description}
 \end{indentblock}
diff -r 242ce8d3d16b -r 6bb3dd7f8097 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jul 15 00:21:32 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jul 15 00:35:07 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, (rel_cases_thm, rel_cases_attrs)) =
+              val (disc_map_iff_thms, sel_map_thms, sel_set_thms (* FIXME: , (rel_cases_thm, rel_cases_attrs) *)) =
                 let
                   val (((Ds, As), Bs), names_lthy) = lthy
                     |> mk_TFrees (dead_of_bnf fp_bnf)
@@ -1407,6 +1407,7 @@
                   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;
@@ -1460,6 +1461,7 @@
                     in
                       (thm, [consumes_attr, case_names_attr, cases_pred_attr ""])
                     end;
+*)
 
                   val disc_map_iff_thms =
                     let
@@ -1583,7 +1585,7 @@
                           |> Proof_Context.export names_lthy lthy
                     end;
                 in
-                  (disc_map_iff_thms, sel_map_thms, sel_set_thms, (rel_cases_thm, rel_cases_attrs))
+                  (disc_map_iff_thms, sel_map_thms, sel_set_thms (* FIXME: , (rel_cases_thm, rel_cases_attrs) *))
                 end;
 
               val anonymous_notes =
@@ -1594,7 +1596,7 @@
               val notes =
                 [(disc_map_iffN, disc_map_iff_thms, simp_attrs),
                  (mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs),
-                 (rel_casesN, [rel_cases_thm], rel_cases_attrs),
+(* FIXME:                 (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 242ce8d3d16b -r 6bb3dd7f8097 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Jul 15 00:21:32 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Jul 15 00:35:07 2014 +0200
@@ -127,12 +127,12 @@
 
 fun mk_disc_map_iff_tac ctxt ct exhaust discs maps =
   TRYALL Goal.conjunction_tac THEN
-    ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
-      REPEAT_DETERM o hyp_subst_tac ctxt) THEN
-    unfold_thms_tac ctxt maps THEN
-    unfold_thms_tac ctxt (map (fn thm => thm RS eqFalseI
-      handle THM _ => thm RS eqTrueI) discs) THEN
-    ALLGOALS (rtac refl ORELSE' rtac TrueI);
+  ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+    REPEAT_DETERM o hyp_subst_tac ctxt) THEN
+  unfold_thms_tac ctxt maps THEN
+  unfold_thms_tac ctxt (map (fn thm => thm RS eqFalseI
+    handle THM _ => thm RS eqTrueI) discs) THEN
+  ALLGOALS (rtac refl ORELSE' rtac TrueI);
 
 fun solve_prem_prem_tac ctxt =
   REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
@@ -225,7 +225,7 @@
     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 =
+    dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses nesting_rel_eqs =
   rtac dtor_rel_coinduct 1 THEN
   EVERY (map11 (fn ct => fn assm => fn exhaust => fn discs => fn sels => fn ctor_defs =>
     fn dtor_ctor => fn ctor_inject => fn abs_inject => fn rel_pre_def => fn abs_inverse =>
@@ -278,8 +278,7 @@
       @{thms not_True_eq_False not_False_eq_True}) THEN
     TRYALL (etac FalseE ORELSE' etac @{thm TrueE}) THEN
     unfold_thms_tac ctxt (sels @ sets) THEN
-    ALLGOALS (
-      REPEAT o (resolve_tac @{thms UnI1 UnI2 imageI} ORELSE'
+    ALLGOALS (REPEAT o (resolve_tac @{thms UnI1 UnI2 imageI} ORELSE'
         eresolve_tac @{thms UN_I UN_I[rotated] imageE} ORELSE'
         hyp_subst_tac ctxt) THEN'
       (rtac @{thm singletonI} ORELSE' atac));