# HG changeset patch
# User blanchet
# Date 1382289608 -7200
# Node ID d7cf4966fafd8a46123d87e42bb5751e901fab43
# Parent  ebdf8deafe1031f208ba96500c8b5f7c37234598
tuning

diff -r ebdf8deafe10 -r d7cf4966fafd src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 20 19:20:08 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 20 19:20:08 2013 +0200
@@ -175,24 +175,21 @@
           if not (member (op =) ctr_args y_head) then
             subst bound_Ts g' $ subst bound_Ts y
           else
-            let
-              val (g, g_args) = strip_comb g';
-              val ctr_pos = try (get_ctr_pos o the) (free_name g) |> the_default ~1;
-              val _ = ctr_pos < 0 orelse length g_args >= ctr_pos orelse
-                primrec_error_eqn "too few arguments in recursive call" t;
-            in
-              (case AList.lookup (op =) nested_calls y_head of
-                SOME y_head' =>
-                massage_nested_rec_call lthy has_call (rewrite_map_arg get_ctr_pos) bound_Ts y_head
-                  y_head' t
-              | NONE =>
-                if ctr_pos >= 0 then
-                  (case AList.lookup (op =) mutual_calls y of
-                    NONE => t
-                  | SOME y' => list_comb (y', g_args))
-                else
-                  t)
-            end
+            (case AList.lookup (op =) nested_calls y_head of
+              SOME y_head' =>
+              massage_nested_rec_call lthy has_call (rewrite_map_arg get_ctr_pos) bound_Ts y_head
+                y_head' t
+            | NONE =>
+              let val (g, g_args) = strip_comb g' in
+                (case try (get_ctr_pos o the) (free_name g) of
+                  SOME ctr_pos =>
+                  (length g_args >= ctr_pos orelse
+                   primrec_error_eqn "too few arguments in recursive call" t;
+                   (case AList.lookup (op =) mutual_calls y of
+                     SOME y' => list_comb (y', g_args)
+                   | NONE => t))
+                | NONE => t)
+              end)
         end
       | subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)
       | subst _ t = t