# HG changeset patch
# User blanchet
# Date 1382133650 -7200
# Node ID 9b25747a134792f49d616b597adce60a5839eac4
# Parent  faa9c35fe79b138667d1c1555412b3993669b363
improve support for recursion through functions

diff -r faa9c35fe79b -r 9b25747a1347 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Oct 18 20:26:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sat Oct 19 00:00:50 2013 +0200
@@ -184,17 +184,18 @@
               val _ = ctr_pos < 0 orelse length g_args >= ctr_pos orelse
                 primrec_error_eqn "too few arguments in recursive call" t;
             in
-              if ctr_pos >= 0 then
-                list_comb (the maybe_mutual_y', g_args)
-              else if is_some maybe_nested_y_head' then
+              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')
+              else if ctr_pos >= 0 then
+                (case maybe_mutual_y' of
+                  NONE => t
+                | SOME y' => list_comb (y', g_args))
               else
                 t
             end
-            |> tap (fn t => tracing ("*** " ^ Syntax.string_of_term lthy t)) (*###*)
         end
       | subst _ t = t
   in