1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sat Oct 26 12:54:39 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sat Oct 26 12:54:57 2013 +0200
     1.3 @@ -159,8 +159,6 @@
     1.4                list_comb (snd_const pT $ nth vs ctr_pos, map (subst d) (nth_drop ctr_pos vs))
     1.5              else
     1.6                primrec_error_eqn ("recursive call not directly applied to constructor argument") t
     1.7 -          else if d = SOME ~1 andalso const_name u = SOME @{const_name comp} then
     1.8 -            list_comb (map_types (K dummyT) u, map2 subst [NONE, d] vs)
     1.9            else
    1.10              list_comb (u, map (subst (d |> d = SOME ~1 ? K NONE)) vs)
    1.11          end

     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Sat Oct 26 12:54:39 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Sat Oct 26 12:54:57 2013 +0200
     2.3 @@ -225,11 +225,13 @@
     2.4        mk_partial_comp (fastype_of g') fT g'
     2.5      end;
     2.6  
     2.7 -fun mk_compN bound_Ts n (g, f) =
     2.8 +fun mk_compN n bound_Ts (g, f) =
     2.9    let val typof = curry fastype_of1 bound_Ts in
    2.10      mk_partial_compN n (typof g) (typof f) g $ f
    2.11    end;
    2.12  
    2.13 +val mk_comp = mk_compN 1;
    2.14 +
    2.15  fun factor_out_types ctxt massage destU U T =
    2.16    (case try destU U of
    2.17      SOME (U1, U2) => if U1 = T then massage T U2 else invalid_map ctxt
    2.18 @@ -245,6 +247,8 @@
    2.19  
    2.20  fun massage_nested_rec_call ctxt has_call raw_massage_fun bound_Ts y y' =
    2.21    let
    2.22 +    fun check_no_call t = if has_call t then unexpected_rec_call ctxt t else ();
    2.23 +
    2.24      val typof = curry fastype_of1 bound_Ts;
    2.25      val build_map_fst = build_map ctxt (fst_const o fst);
    2.26  
    2.27 @@ -255,8 +259,12 @@
    2.28      val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t);
    2.29  
    2.30      fun massage_mutual_fun U T t =
    2.31 -      if has_call t then factor_out_types ctxt raw_massage_fun HOLogic.dest_prodT U T t
    2.32 -      else HOLogic.mk_comp (t, build_map_fst (U, T));
    2.33 +      (case t of
    2.34 +        Const (@{const_name comp}, comp_T) $ t1 $ t2 =>
    2.35 +        mk_comp bound_Ts (tap check_no_call t1, massage_mutual_fun U T t2)
    2.36 +      | _ =>
    2.37 +        if has_call t then factor_out_types ctxt raw_massage_fun HOLogic.dest_prodT U T t
    2.38 +        else mk_comp bound_Ts (t, build_map_fst (U, T)));
    2.39  
    2.40      fun massage_map (Type (_, Us)) (Type (s, Ts)) t =
    2.41          (case try (dest_map ctxt s) t of
    2.42 @@ -272,7 +280,7 @@
    2.43        | massage_map _ _ t = raise AINT_NO_MAP t
    2.44      and massage_map_or_map_arg U T t =
    2.45        if T = U then
    2.46 -        if has_call t then unexpected_rec_call ctxt t else t
    2.47 +        tap check_no_call t
    2.48        else
    2.49          massage_map U T t
    2.50          handle AINT_NO_MAP _ => massage_mutual_fun U T t;
    2.51 @@ -286,7 +294,7 @@
    2.52              let val (g, xs) = Term.strip_comb t2 in
    2.53                if g = y then
    2.54                  if exists has_call xs then unexpected_rec_call ctxt t2
    2.55 -                else Term.list_comb (massage_call (mk_compN bound_Ts (length xs) (t1, y)), xs)
    2.56 +                else Term.list_comb (massage_call (mk_compN (length xs) bound_Ts (t1, y)), xs)
    2.57                else
    2.58                  ill_formed_rec_call ctxt t
    2.59              end
    2.60 @@ -411,7 +419,7 @@
    2.61      fun massage_mutual_fun bound_Ts U T t =
    2.62        (case t of
    2.63          Const (@{const_name comp}, comp_T) $ t1 $ t2 =>
    2.64 -        mk_compN bound_Ts 1 (massage_mutual_fun bound_Ts U T t1, tap check_no_call t2)
    2.65 +        mk_comp bound_Ts (massage_mutual_fun bound_Ts U T t1, tap check_no_call t2)
    2.66        | _ =>
    2.67          let
    2.68            val var = Var ((Name.uu, Term.maxidx_of_term t + 1),