# HG changeset patch
# User blanchet
# Date 1382286179 -7200
# Node ID 6e01e29d34bc5f67a31fe05fa2bec60d565bfc7d
# Parent  800106c1741954c5c5b53456fbd46fccdfaa47b9
simplify code

diff -r 800106c17419 -r 6e01e29d34bc src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 20 17:45:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 20 18:22:59 2013 +0200
@@ -185,10 +185,8 @@
                 primrec_error_eqn "too few arguments in recursive call" t;
             in
               if is_some maybe_nested_y_head' then
-                (if has_call g' then t else y)
-                |> massage_nested_rec_call lthy has_call
-                  (rewrite_map_arg get_ctr_pos) bound_Ts y_head (the maybe_nested_y_head')
-                |> (if has_call g' then I else curry (op $) g')
+                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