# HG changeset patch
# User blanchet
# Date 1366805116 -7200
# Node ID 587bba4254302577d853bd53b2db0e477562b811
# Parent  55963309557b67080230ca7a14a5a745986200a4
eta-contracted weak congruence rules (like in the old package)

diff -r 55963309557b -r 587bba425430 src/HOL/BNF/Tools/bnf_wrap.ML
--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Wed Apr 24 13:16:21 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Wed Apr 24 14:05:16 2013 +0200
@@ -197,15 +197,23 @@
     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 eta_fcase = Term.list_comb (casex, eta_fs);
+    val eta_gcase = Term.list_comb (casex, eta_gs);
 
-    val ufcase = fcase $ u;
-    val vfcase = fcase $ v;
-    val vgcase = gcase $ v;
+    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);
 
@@ -346,7 +354,7 @@
 
     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];
 
@@ -548,7 +556,7 @@
               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)]
@@ -568,7 +576,7 @@
 
             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),
@@ -584,7 +592,7 @@
               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));