# HG changeset patch
# User panny
# Date 1383045180 -3600
# Node ID ab0595cb9fe9b2edb24fd06903e2b7c5217ab91e
# Parent  6d0688ce4ee2d106861c792e4ed66def6992d7e1
include corecursive functions' arguments in callssss

diff -r 6d0688ce4ee2 -r ab0595cb9fe9 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Tue Oct 29 08:06:08 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Tue Oct 29 12:13:00 2013 +0100
@@ -281,10 +281,10 @@
       bs mxs
   end;
 
-fun massage_comp ctxt has_call bound_Ts t =
+fun massage_comp ctxt has_call bound_Ts t = (* FIXME unused *)
   massage_nested_corec_call ctxt has_call (K (K (K I))) bound_Ts (fastype_of1 (bound_Ts, t)) t;
 
-fun find_rec_calls ctxt has_call (eqn_data : eqn_data) =
+fun find_rec_calls ctxt has_call ({ctr, ctr_args, rhs_term, ...} : eqn_data) =
   let
     fun find bound_Ts (Abs (_, T, b)) ctr_arg = find (T :: bound_Ts) b ctr_arg
       | find bound_Ts (t as _ $ _) ctr_arg =
@@ -309,8 +309,8 @@
         end
       | find _ _ _ = [];
   in
-    map (find [] (#rhs_term eqn_data)) (#ctr_args eqn_data)
-    |> (fn [] => NONE | callss => SOME (#ctr eqn_data, callss))
+    map (find [] rhs_term) ctr_args
+    |> (fn [] => NONE | callss => SOME (ctr, callss))
   end;
 
 fun prepare_primrec fixes specs lthy =
@@ -704,7 +704,7 @@
           let val (u, vs) = strip_comb t in
             if is_Free u andalso has_call u then
               Inr_const U T $ mk_tuple1 bound_Ts vs
-            else if try (fst o dest_Const) u = SOME @{const_name prod_case} then
+            else if const_name u = SOME @{const_name prod_case} then
               map (rewrite bound_Ts U T) vs |> chop 1 |>> HOLogic.mk_split o the_single |> list_comb
             else
               list_comb (rewrite bound_Ts U T u, map (rewrite bound_Ts U T) vs)
@@ -807,7 +807,13 @@
     val sel_no = find_first (equal ctr o #ctr) basic_ctr_specs
       |> find_index (equal sel) o #sels o the;
     fun find (Abs (_, _, b)) = find b
-      | find (t as _ $ _) = strip_comb t |>> find ||> maps find |> (op @)
+      | find (t as _ $ _) =
+        let val (f, args as arg :: _) = strip_comb t in
+          if is_Free f andalso has_call f orelse is_Free arg andalso has_call arg then
+            [t]
+          else
+            find f @ maps find args
+        end
       | find f = if is_Free f andalso has_call f then [f] else [];
   in
     find rhs_term