src/HOL/BNF/Tools/bnf_wrap.ML

--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Wed Sep 26 10:01:00 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Wed Sep 26 10:01:00 2012 +0200
@@ -35,9 +35,9 @@
 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";
@@ -382,7 +382,7 @@
           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
@@ -539,18 +539,18 @@
                   |> 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) =
@@ -601,9 +601,9 @@
         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, []),