src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

 val ctr_transferN = "ctr_transfer";
 val corec_codeN = "corec_code";
 val map_disc_iffN = "map_disc_iff";
 val map_selN = "map_sel";
 val set_casesN = "set_cases";
-val set_emptyN = "set_empty";
 val set_introsN = "set_intros";
 val set_inductN = "set_induct";
 val set_selN = "set_sel";
 
 structure Data = Generic_Data

               val set0_thms = flat set0_thmss;
               val set_thms = set0_thms
                 |> map (unfold_thms lthy @{thms insert_is_Un[THEN sym] Un_empty_left
                   Un_insert_left});
 
-              val sets = map (mk_set (snd (Term.dest_Type fpT))) (sets_of_bnf fp_bnf);
-
-              val set_empty_thms =
-                let
-                  val ctr_argT_namess = map ((fn Ts => fold Term.add_tfree_namesT Ts []) o
-                    binder_types o fastype_of) ctrs;
-                  val setTs = map (HOLogic.dest_setT o range_type o fastype_of) sets;
-                  val setT_names = map (fn T => the_single (Term.add_tfree_namesT T [])) setTs;
-
-                  fun mk_set_empty_goal disc set T =
-                    Logic.mk_implies (HOLogic.mk_Trueprop (disc $ u),
-                      mk_Trueprop_eq (set $ u, HOLogic.mk_set T []));
-
-                  val goals =
-                    if null discs then
-                      []
-                    else
-                      map_filter I (flat
-                        (map2 (fn names => fn disc =>
-                          map3 (fn name => fn setT => fn set =>
-                            if member (op =) names name then NONE
-                            else SOME (mk_set_empty_goal disc set setT))
-                          setT_names setTs sets)
-                        ctr_argT_namess discs));
-                in
-                  if null goals then
-                    []
-                  else
-                    Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
-                      (fn {context = ctxt, prems = _} =>
-                        mk_set_empty_tac ctxt (certify ctxt u) exhaust set0_thms (flat disc_thmss))
-                    |> Conjunction.elim_balanced (length goals)
-                    |> Proof_Context.export names_lthy lthy
-                    |> map Thm.close_derivation
-                end;
-
               val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns);
 
               fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
                 fold_thms lthy ctr_defs'
                   (unfold_thms lthy (pre_rel_def :: abs_inverse ::

                   val ctr_transfer_thms =
                     let
                       val goals = mk_parametricity_goals names_lthy Rs ctrAs ctrBs;
                     in
                       Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
-                        (fn {context = ctxt, prems = _} => mk_ctr_transfer_tac rel_intro_thms)
+                        (K (mk_ctr_transfer_tac rel_intro_thms))
                       |> Conjunction.elim_balanced (length goals)
                       |> Proof_Context.export names_lthy lthy
                       |> map Thm.close_derivation
                     end;
 

                               end) ctrAs;
                           val goal = Logic.mk_implies (mk_Trueprop_mem (elem, set $ ta), thesis);
                           val thm =
                             Goal.prove_sorry lthy [] (flat premss) goal
                               (fn {context = ctxt, prems} =>
-                                mk_set_cases_tac ctxt (certify ctxt ta) prems exhaust set_thms)
+                                 mk_set_cases_tac ctxt (certify ctxt ta) prems exhaust set_thms)
                             |> singleton (Proof_Context.export names_lthy lthy)
                             |> Thm.close_derivation
                             |> rotate_prems ~1;
 
                           val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));

                       if null goals then
                         []
                       else
                         Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
                           (fn {context = ctxt, prems = _} =>
-                            mk_rel_sel_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
-                              (flat disc_thmss) (flat sel_thmss) rel_inject_thms distincts
-                              rel_distinct_thms)
+                             mk_rel_sel_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
+                               (flat disc_thmss) (flat sel_thmss) rel_inject_thms distincts
+                               rel_distinct_thms)
                         |> Conjunction.elim_balanced (length goals)
                         |> Proof_Context.export names_lthy lthy
                         |> map Thm.close_derivation
                     end;
 

                       val goal =
                         Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms, thesis);
                       val thm =
                         Goal.prove_sorry lthy [] [] goal
                           (fn {context = ctxt, prems = _} =>
-                            mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
-                              injects rel_inject_thms distincts rel_distinct_thms
-                              (map rel_eq_of_bnf live_nesting_bnfs))
+                             mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
+                               injects rel_inject_thms distincts rel_distinct_thms
+                               (map rel_eq_of_bnf live_nesting_bnfs))
                         |> singleton (Proof_Context.export names_lthy lthy)
                         |> Thm.close_derivation;
 
                       val ctr_names = quasi_unambiguous_case_names ((map name_of_ctr) ctrAs);
                       val case_names_attr = Attrib.internal (K (Rule_Cases.case_names ctr_names));

                       if null goals then
                         []
                       else
                         Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
                           (fn {context = ctxt, prems = _} =>
-                            mk_map_disc_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
-                              map_thms)
+                             mk_map_disc_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
+                               map_thms)
                         |> Conjunction.elim_balanced (length goals)
                         |> Proof_Context.export names_lthy lthy
                         |> map Thm.close_derivation
                     end;
 

                           val concl = mk_Trueprop_eq (lhs, rhs);
                         in
                           if is_refl_bool prem then concl
                           else Logic.mk_implies (HOLogic.mk_Trueprop prem, concl)
                         end;
+
                       val goals = map mk_goal discAs_selAss;
                     in
                       if null goals then
                         []
                       else
                         Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
                           (fn {context = ctxt, prems = _} =>
-                            mk_map_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
-                              map_thms (flat sel_thmss))
+                             mk_map_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
+                               map_thms (flat sel_thmss))
                         |> Conjunction.elim_balanced (length goals)
                         |> Proof_Context.export names_lthy lthy
                         |> map Thm.close_derivation
                     end;
 

                  (rel_injectN, rel_inject_thms, K simp_attrs),
                  (rel_introsN, rel_intro_thms, K []),
                  (rel_selN, rel_sel_thms, K []),
                  (setN, set_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
                  (set_casesN, set_cases_thms, nth set_cases_attrss),
-                 (set_emptyN, set_empty_thms, K []),
                  (set_introsN, set_intros_thms, K []),
                  (set_selN, set_sel_thms, K [])]
                 |> massage_simple_notes fp_b_name;
 
               val (noted, lthy') =