# HG changeset patch
# User blanchet
# Date 1366872997 -7200
# Node ID 78162d9e977d5c493c7b55580fc18f45cf6e59f2
# Parent  5c657ca97d992a870aec9fb89d24f1f83f2a4679
no eta-expansion for case in split rules and case_conv

diff -r 5c657ca97d99 -r 78162d9e977d src/HOL/BNF/Tools/bnf_wrap.ML
--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Apr 25 08:56:10 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Apr 25 08:56:37 2013 +0200
@@ -212,7 +212,6 @@
     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);
@@ -354,7 +353,7 @@
 
     val cases_goal =
       map3 (fn xs => fn xctr => fn xf =>
-        fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (eta_fcase $ xctr, xf))) xss xctrs xfs;
+        fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xss xctrs xfs;
 
     val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss @ [cases_goal];
 
@@ -556,7 +555,7 @@
               val case_conv_thms =
                 let
                   fun mk_body f usels = Term.list_comb (f, usels);
-                  val goal = mk_Trueprop_eq (eta_ufcase, mk_IfN B udiscs (map2 mk_body fs uselss));
+                  val goal = mk_Trueprop_eq (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)]
@@ -592,7 +591,7 @@
               list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr),
                 HOLogic.mk_not (q $ f_xs)));
 
-            val lhs = q $ eta_ufcase;
+            val lhs = q $ ufcase;
 
             val goal =
               mk_Trueprop_eq (lhs, Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct xctrs xss xfs));