1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Oct 18 19:03:39 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Fri Oct 18 19:18:32 2013 +0200
     1.3 @@ -172,27 +172,30 @@
     1.4    let
     1.5      fun subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)
     1.6        | subst bound_Ts (t as g' $ y) =
     1.7 -        if not (member (op =) ctr_args y) then
     1.8 -          pairself (subst bound_Ts) (g', y) |> op $
     1.9 -        else
    1.10 -          let
    1.11 -            val maybe_mutual_y' = AList.lookup (op =) mutual_calls y;
    1.12 -            val maybe_nested_y' = AList.lookup (op =) nested_calls y;
    1.13 -            val (g, g_args) = strip_comb g';
    1.14 -            val ctr_pos = try (get_ctr_pos o the) (free_name g) |> the_default ~1;
    1.15 -            val _ = ctr_pos < 0 orelse length g_args >= ctr_pos orelse
    1.16 -              primrec_error_eqn "too few arguments in recursive call" t;
    1.17 -          in
    1.18 -            if ctr_pos >= 0 then
    1.19 -              list_comb (the maybe_mutual_y', g_args)
    1.20 -            else if is_some maybe_nested_y' then
    1.21 -              (if has_call g' then t else y)
    1.22 -              |> massage_nested_rec_call lthy has_call
    1.23 -                (rewrite_map_arg get_ctr_pos) bound_Ts y (the maybe_nested_y')
    1.24 -              |> (if has_call g' then I else curry (op $) g')
    1.25 -            else
    1.26 -              t
    1.27 -          end
    1.28 +        let val y_head = head_of y in
    1.29 +          if not (member (op =) ctr_args y_head) then
    1.30 +            pairself (subst bound_Ts) (g', y) |> op $
    1.31 +          else
    1.32 +            let
    1.33 +              val maybe_mutual_y' = AList.lookup (op =) mutual_calls y;
    1.34 +              val maybe_nested_y_head' = AList.lookup (op =) nested_calls y_head;
    1.35 +              val (g, g_args) = strip_comb g';
    1.36 +              val ctr_pos = try (get_ctr_pos o the) (free_name g) |> the_default ~1;
    1.37 +              val _ = ctr_pos < 0 orelse length g_args >= ctr_pos orelse
    1.38 +                primrec_error_eqn "too few arguments in recursive call" t;
    1.39 +            in
    1.40 +              if ctr_pos >= 0 then
    1.41 +                list_comb (the maybe_mutual_y', g_args)
    1.42 +              else if is_some maybe_nested_y_head' then
    1.43 +                (if has_call g' then t else y)
    1.44 +                |> massage_nested_rec_call lthy has_call
    1.45 +                  (rewrite_map_arg get_ctr_pos) bound_Ts y_head (the maybe_nested_y_head')
    1.46 +                |> (if has_call g' then I else curry (op $) g')
    1.47 +              else
    1.48 +                t
    1.49 +            end
    1.50 +            |> tap (fn t => tracing ("*** " ^ Syntax.string_of_term lthy t)) (*###*)
    1.51 +        end
    1.52        | subst _ t = t
    1.53    in
    1.54      subst [] t
    1.55 @@ -583,7 +586,7 @@
    1.56        else apfst SOME (dissect_coeqn_disc seq fun_names basic_ctr_specss
    1.57            (SOME (abstract (List.rev fun_args) rhs)) maybe_code_rhs prems disc_concl matchedsss);
    1.58  
    1.59 -    val sel_concls = (sels ~~ ctr_args)
    1.60 +    val sel_concls = sels ~~ ctr_args
    1.61        |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg));
    1.62  
    1.63  (*
    1.64 @@ -838,7 +841,8 @@
    1.65        map_filter (try (fn Sel x => x)) eqns_data
    1.66        |> partition_eq ((op =) o pairself #fun_name)
    1.67        |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
    1.68 -      |> map (flat o snd)      |> map2 (fold o find_corec_calls has_call) basic_ctr_specss
    1.69 +      |> map (flat o snd)
    1.70 +      |> map2 (fold o find_corec_calls has_call) basic_ctr_specss
    1.71        |> map2 (curry (op |>)) (map (map (fn {ctr, sels, ...} =>
    1.72          (ctr, map (K []) sels))) basic_ctr_specss);
    1.73