src/HOL/BNF/Tools/bnf_wrap.ML

 val isN = "is_";
 val unN = "un_";
 fun mk_unN 1 1 suf = unN ^ suf
   | mk_unN _ l suf = unN ^ suf ^ string_of_int l;
 
+val caseN = "case";
 val case_congN = "case_cong";
-val case_eqN = "case_eq";
-val casesN = "cases";
+val case_convN = "case_conv";
 val collapseN = "collapse";
 val disc_excludeN = "disc_exclude";
 val disc_exhaustN = "disc_exhaust";
 val discsN = "discs";
 val distinctN = "distinct";

           in
             Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm)
           end;
 
         val (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
-             disc_exhaust_thms, collapse_thms, expand_thms, case_eq_thms) =
+             disc_exhaust_thms, collapse_thms, expand_thms, case_conv_thms) =
           if no_dests then
             ([], [], [], [], [], [], [], [], [], [])
           else
             let
               fun make_sel_thm xs' case_thm sel_def =

                        (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
                        disc_exclude_thmsss')]
                   |> Proof_Context.export names_lthy lthy
                 end;
 
-              val case_eq_thms =
+              val case_conv_thms =
                 let
                   fun mk_body f usels = Term.list_comb (f, usels);
                   val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs (map2 mk_body fs uselss));
                 in
                   [Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
-                     mk_case_eq_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)]
+                     mk_case_conv_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)]
                   |> Proof_Context.export names_lthy lthy
                 end;
             in
               (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
-               [disc_exhaust_thm], collapse_thms, expand_thms, case_eq_thms)
+               [disc_exhaust_thm], collapse_thms, expand_thms, case_conv_thms)
             end;
 
         val (case_cong_thm, weak_case_cong_thm) =
           let
             fun mk_prem xctr xs f g =

 
         val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
         val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name));
 
         val notes =
-          [(case_congN, [case_cong_thm], []),
-           (case_eqN, case_eq_thms, []),
-           (casesN, case_thms, simp_attrs),
+          [(caseN, case_thms, simp_attrs),
+           (case_congN, [case_cong_thm], []),
+           (case_convN, case_conv_thms, []),
            (collapseN, collapse_thms, simp_attrs),
            (discsN, disc_thms, simp_attrs),
            (disc_excludeN, disc_exclude_thms, []),
            (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
            (distinctN, distinct_thms, simp_attrs @ induct_simp_attrs),