# HG changeset patch
# User blanchet
# Date 1381739236 -7200
# Node ID 81c2062b91de2502a98dae4ace4f0e4e9f0d460d
# Parent  89a4c9b3ed62633ebd5a3317a30125ff6860dfd5
tuning

diff -r 89a4c9b3ed62 -r 81c2062b91de src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Oct 14 10:06:03 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Oct 14 10:27:16 2013 +0200
@@ -295,8 +295,8 @@
 
     fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else ();
 
-    fun beta_contract (t as Abs (_, T, f $ Bound 0)) = incr_boundvars ~1 f
-      | beta_contract (t as Abs (v, T, b)) = Abs (v, T, beta_contract b);
+    fun eta_contr (t as Abs (_, T, f $ Bound 0)) = incr_boundvars ~1 f
+      | eta_contr (t as Abs (v, T, b)) = Abs (v, T, eta_contr b);
     fun massage_abs bound_Ts (Abs (s, T, t)) = Abs (s, T, massage_abs (T :: bound_Ts) t)
       | massage_abs bound_Ts t = massage_rec bound_Ts t
     and massage_rec bound_Ts t =
@@ -308,12 +308,12 @@
           let val branches' = map (massage_rec bound_Ts) branches in
             Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches')
           end
-        | (Const (c, c_T), args as _ :: _ :: _) =>
+        | (Const (c, T), args as _ :: _ :: _) =>
           let
             val gen_T = Sign.the_const_type thy c;
             val (gen_branch_Ts, gen_body_fun_T) = strip_fun_type gen_T;
             val n = length gen_branch_Ts;
-            val n_res_T = strip_typeN n c_T |> length o binder_types o snd;
+            val n_res_T = strip_typeN n T |> length o binder_types o snd;
           in
             if n < length args then
               (case gen_body_fun_T of
@@ -321,7 +321,7 @@
                 if case_of ctxt T_name = SOME c then
                   let
                     val (branches, obj_leftovers) = chop n args;
-                    val branches' = map (massage_abs bound_Ts o funpow (n_res_T - 1) beta_contract o
+                    val branches' = map (massage_abs bound_Ts o funpow (n_res_T - 1) eta_contr o
                       Envir.eta_long bound_Ts) branches;
                     val branch_Ts' = map typof branches';
                     val casex' = Const (c, branch_Ts' ---> map typof obj_leftovers --->