src/HOL/BNF/Tools/bnf_wrap.ML

     val yctrs = map2 (curry Term.list_comb) ctrs yss;
 
     val xfs = map2 (curry Term.list_comb) fs xss;
     val xgs = map2 (curry Term.list_comb) gs xss;
 
+    val fcase = Term.list_comb (casex, fs);
+    val gcase = Term.list_comb (casex, gs);
+
+    val ufcase = fcase $ u;
+    val vfcase = fcase $ v;
+
+    (* TODO: Eta-expension is for compatibility with the old datatype package (but it also provides
+       nicer names). Consider removing. *)
     val eta_fs = map2 eta_expand_arg xss xfs;
     val eta_gs = map2 eta_expand_arg xss xgs;
 
-    val fcase = Term.list_comb (casex, eta_fs);
-    val gcase = Term.list_comb (casex, eta_gs);
-
-    val ufcase = fcase $ u;
-    val vfcase = fcase $ v;
-    val vgcase = gcase $ v;
+    val eta_fcase = Term.list_comb (casex, eta_fs);
+    val eta_gcase = Term.list_comb (casex, eta_gs);
+
+    val eta_ufcase = eta_fcase $ u;
+    val eta_vfcase = eta_fcase $ v;
+    val eta_vgcase = eta_gcase $ v;
 
     fun mk_uu_eq () = HOLogic.mk_eq (u, u);
 
     val uv_eq = mk_Trueprop_eq (u, v);
 

         map (map mk_goal) (mk_half_pairss (`I (xss ~~ xctrs)))
       end;
 
     val cases_goal =
       map3 (fn xs => fn xctr => fn xf =>
-        fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xss xctrs xfs;
+        fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (eta_fcase $ xctr, xf))) xss xctrs xfs;
 
     val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss @ [cases_goal];
 
     fun after_qed thmss lthy =
       let

                 end;
 
               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));
+                  val goal = mk_Trueprop_eq (eta_ufcase, mk_IfN B udiscs (map2 mk_body fs uselss));
                 in
                   [Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
                      mk_case_conv_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)]
                   |> map Thm.close_derivation
                   |> Proof_Context.export names_lthy lthy

               fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr),
                 mk_Trueprop_eq (f, g)));
 
             val goal =
               Logic.list_implies (uv_eq :: map4 mk_prem xctrs xss fs gs,
-                 mk_Trueprop_eq (ufcase, vgcase));
+                 mk_Trueprop_eq (eta_ufcase, eta_vgcase));
             val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase));
           in
             (Goal.prove_sorry lthy [] [] goal (fn _ => mk_case_cong_tac lthy uexhaust_thm case_thms),
              Goal.prove_sorry lthy [] [] weak_goal (K (etac arg_cong 1)))
             |> pairself (Thm.close_derivation #> singleton (Proof_Context.export names_lthy lthy))

               list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (u, xctr), q $ f_xs));
             fun mk_disjunct xctr xs f_xs =
               list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr),
                 HOLogic.mk_not (q $ f_xs)));
 
-            val lhs = q $ ufcase;
+            val lhs = q $ eta_ufcase;
 
             val goal =
               mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs));
             val asm_goal =
               mk_Trueprop_eq (lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj