# HG changeset patch
# User blanchet
# Date 1380121289 -7200
# Node ID 865da57dee932430a3cbe7440707456e72d9f01b
# Parent  c54ebf9dbd34d0e809be9f3c465da3cd5e84c688
further improved 'code' helper functions

diff -r c54ebf9dbd34 -r 865da57dee93 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 16:57:48 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 17:01:29 2013 +0200
@@ -255,12 +255,14 @@
 
     fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else ();
 
-    fun massage_rec bound_Ts t =
+    fun massage_abs bound_Ts (Abs (s, T, t)) = massage_abs (T :: bound_Ts) t
+      | massage_abs bound_Ts t = massage_rec bound_Ts t
+    and massage_rec bound_Ts t =
       let val typof = curry fastype_of1 bound_Ts in
         (case Term.strip_comb t of
           (Const (@{const_name Let}, _), [arg1, arg2]) =>
           massage_rec bound_Ts (betapply (arg2, arg1))
-        | (Const (@{const_name If}, _), obj :: (branches as [then_branch, _])) =>
+        | (Const (@{const_name If}, _), obj :: (branches as [_, _])) =>
           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
@@ -272,7 +274,7 @@
                 if case_of ctxt s = SOME c then
                   let
                     val (branches, obj_leftovers) = chop n args;
-                    val branches' = map (massage_rec bound_Ts) branches;
+                    val branches' = map (massage_abs bound_Ts o Envir.eta_long bound_Ts) branches;
                     val casex' = Const (c, map typof branches' ---> map typof obj_leftovers --->
                       typof t);
                   in
@@ -370,7 +372,7 @@
 fun expand_corec_code_rhs ctxt has_call bound_Ts t =
   (case fastype_of1 (bound_Ts, t) of
     Type (s, Ts) =>
-    massage_let_if_case ctxt has_call (fn bound_Ts => fn t =>
+    massage_let_if_case ctxt has_call (fn _ => fn t =>
       if can (dest_ctr ctxt s) t then t else expand_ctr_term ctxt s Ts t) bound_Ts t
   | _ => raise Fail "expand_corec_code_rhs");