# HG changeset patch
# User blanchet
# Date 1410454476 -7200
# Node ID a0fe6d8c8ba2541a9cb41a8e797d07e57dba9809
# Parent  c59f6a31001ea67e5421dfbedf63dbbd0bf61b32
fixed situation in 'primrec' when recursive calls are apparently nested, e.g. 'f (f x y) y', with the recursion in 'y'

diff -r c59f6a31001e -r a0fe6d8c8ba2 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Thu Sep 11 18:54:36 2014 +0200
@@ -301,27 +301,27 @@
 
     fun subst bound_Ts (t as g' $ y) =
         let
-          fun subst_rec (h $ z) = subst bound_Ts h $ subst bound_Ts z
-            | subst_rec t = t;
+          fun subst_comb (h $ z) = subst bound_Ts h $ subst bound_Ts z
+            | subst_comb t = t;
 
           val y_head = head_of y;
         in
           if not (member (op =) ctr_args y_head) then
-            subst_rec t
+            subst_comb t
           else
             (case try_nested_rec bound_Ts y_head t of
-              SOME t' => subst_rec t'
+              SOME t' => subst_comb t'
             | NONE =>
               let val (g, g_args) = strip_comb g' in
                 (case try (get_ctr_pos o fst o dest_Free) g of
-                  SOME ~1 => subst_rec t
+                  SOME ~1 => subst_comb t
                 | SOME ctr_pos =>
                   (length g_args >= ctr_pos orelse
                    raise PRIMREC ("too few arguments in recursive call", [t]);
                    (case AList.lookup (op =) mutual_calls y of
-                     SOME y' => list_comb (y', g_args)
-                   | NONE => subst_rec t))
-                | NONE => subst_rec t)
+                     SOME y' => list_comb (y', map (subst bound_Ts) g_args)
+                   | NONE => subst_comb t))
+                | NONE => subst_comb t)
               end)
         end
       | subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)
@@ -329,7 +329,6 @@
 
     fun subst' t =
       if has_call t then
-        (* FIXME detect this case earlier? *)
         raise PRIMREC ("recursive call not directly applied to constructor argument", [t])
       else
         try_nested_rec [] (head_of t) t |> the_default t