# HG changeset patch
# User panny
# Date 1377891795 -7200
# Node ID 585b2fee55e503079945984d4aac93854018bbdc
# Parent  646a224ca76a890ad9b84df8597b4ac85817fb9b
fixed bug in primrec_new (allow indirect recursion through constructor arguments other than the first)

diff -r 646a224ca76a -r 585b2fee55e5 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Aug 30 21:14:38 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Aug 30 21:43:15 2013 +0200
@@ -714,10 +714,17 @@
 Explain @{const lmap}.
 *}
 
-    primrec_new_notyet sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" where
+(*<*)
+    locale sum_btree_nested
+      begin
+(*>*)
+    primrec_new sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" where
       "sum_btree (BNode a lt rt) =
          a + the_default 0 (option_map sum_btree lt) +
            the_default 0 (option_map sum_btree rt)"
+(*<*)
+    end
+(*>*)
 
 text {*
 Show example with function composition (ftree).
diff -r 646a224ca76a -r 585b2fee55e5 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Aug 30 21:14:38 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Aug 30 21:43:15 2013 +0200
@@ -173,14 +173,17 @@
       massage_indirect_rec_call lthy (not o null o get_indices) massage_map_arg bound_Ts y y';
     fun subst bound_Ts (t as _ $ _) =
         let
+          val ctr_args = fold_aterms (curry (op @) o get_indices) t []
+            |> maps (maps #ctr_args o nth funs_data);
           val (f', args') = strip_comb t;
           val fun_arg_idx = find_index (exists_subterm (not o null o get_indices)) args';
           val arg_idx = find_index (exists_subterm (equal y)) args';
           val (f, args) = chop (arg_idx + 1) args' |>> curry list_comb f';
           val _ = fun_arg_idx < 0 orelse arg_idx >= 0 orelse
+            exists (exists_subterm (member (op =) ctr_args)) args' orelse
             primrec_error_eqn "recursive call not applied to constructor argument" t;
         in
-          if fun_arg_idx <> arg_idx andalso fun_arg_idx >= 0 then
+          if fun_arg_idx <> arg_idx andalso fun_arg_idx >= 0 andalso arg_idx >= 0 then
             if nth args' arg_idx = y then
               list_comb (massage (rewrite_map_arg funs_data get_indices y) bound_Ts f, args)
             else