# HG changeset patch
# User blanchet
# Date 1382289608 -7200
# Node ID 5086aac9684694307d3ea10fcc5d77637e32ad50
# Parent  6e01e29d34bc5f67a31fe05fa2bec60d565bfc7d
tuning

diff -r 6e01e29d34bc -r 5086aac96846 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 20 18:22:59 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 20 19:20:08 2013 +0200
@@ -170,11 +170,10 @@
 
 fun subst_rec_calls lthy get_ctr_pos has_call ctr_args mutual_calls nested_calls t =
   let
-    fun subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)
-      | subst bound_Ts (t as g' $ y) =
+    fun subst bound_Ts (t as g' $ y) =
         let val y_head = head_of y in
           if not (member (op =) ctr_args y_head) then
-            pairself (subst bound_Ts) (g', y) |> op $
+            subst bound_Ts g' $ subst bound_Ts y
           else
             let
               val maybe_mutual_y' = AList.lookup (op =) mutual_calls y;
@@ -185,8 +184,8 @@
                 primrec_error_eqn "too few arguments in recursive call" t;
             in
               if is_some maybe_nested_y_head' then
-                massage_nested_rec_call lthy has_call
-                  (rewrite_map_arg get_ctr_pos) bound_Ts y_head (the maybe_nested_y_head') t
+                massage_nested_rec_call lthy has_call (rewrite_map_arg get_ctr_pos) bound_Ts y_head
+                  (the maybe_nested_y_head') t
               else if ctr_pos >= 0 then
                 (case maybe_mutual_y' of
                   NONE => t
@@ -195,6 +194,7 @@
                 t
             end
         end
+      | subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)
       | subst _ t = t
   in
     subst [] t