1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Fri Oct 18 19:18:32 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Fri Oct 18 20:26:46 2013 +0200
     1.3 @@ -215,19 +215,6 @@
     1.4      SOME (U1, U2) => if U1 = T then massage T U2 else invalid_map ctxt
     1.5    | NONE => invalid_map ctxt);
     1.6  
     1.7 -fun expand_to_comp bound_Ts f t =
     1.8 -  let
     1.9 -    val (g, xs) = Term.strip_comb t;
    1.10 -    val m = length xs;
    1.11 -    val j = Term.maxidx_of_term t;
    1.12 -    val us = map2 (fn k => fn x => Var ((Name.uu, j + k), fastype_of1 (bound_Ts, x))) (1 upto m) xs;
    1.13 -    val u_tuple = HOLogic.mk_tuple us;
    1.14 -    val unc_g = mk_tupled_fun u_tuple g us;
    1.15 -    val x_tuple = HOLogic.mk_tuple xs;
    1.16 -  in
    1.17 -    (HOLogic.mk_comp (f, unc_g), x_tuple)
    1.18 -  end;
    1.19 -
    1.20  fun map_flattened_map_args ctxt s map_args fs =
    1.21    let
    1.22      val flat_fs = flatten_type_args_of_bnf (the (bnf_of ctxt s)) Term.dummy fs;
    1.23 @@ -236,6 +223,22 @@
    1.24      permute_like (op aconv) flat_fs fs flat_fs'
    1.25    end;
    1.26  
    1.27 +fun mk_partial_comp gT fT g =
    1.28 +  let val T = domain_type fT --> range_type gT in
    1.29 +    Const (@{const_name Fun.comp}, gT --> fT --> T) $ g
    1.30 +  end;
    1.31 +
    1.32 +fun mk_compN' 0 _ _ g = g
    1.33 +  | mk_compN' n gT fT g =
    1.34 +    let val g' = mk_compN' (n - 1) gT (range_type fT) g in
    1.35 +      mk_partial_comp (fastype_of g') fT g'
    1.36 +    end;
    1.37 +
    1.38 +fun mk_compN bound_Ts n (g, f) =
    1.39 +  let val typof = curry fastype_of1 bound_Ts in
    1.40 +    mk_compN' n (typof g) (typof f) g $ f
    1.41 +  end;
    1.42 +
    1.43  fun massage_nested_rec_call ctxt has_call raw_massage_fun bound_Ts y y' =
    1.44    let
    1.45      val typof = curry fastype_of1 bound_Ts;
    1.46 @@ -274,13 +277,14 @@
    1.47          if t2 = y then
    1.48            massage_map yU yT (elim_y t1) $ y'
    1.49            handle AINT_NO_MAP t' => invalid_map ctxt t'
    1.50 -        else if head_of t2 = y then
    1.51 -          let val (u1, u2) = expand_to_comp bound_Ts t1 t2 in
    1.52 -            if has_call u2 then unexpected_rec_call ctxt u2
    1.53 -            else massage_call u1 $ u2
    1.54 +        else
    1.55 +          let val (g, xs) = Term.strip_comb t2 in
    1.56 +            if g = y then
    1.57 +              if exists has_call xs then unexpected_rec_call ctxt t2
    1.58 +              else Term.list_comb (massage_call (mk_compN bound_Ts (length xs) (t1, y)), xs)
    1.59 +            else
    1.60 +              ill_formed_rec_call ctxt t
    1.61            end
    1.62 -        else
    1.63 -          ill_formed_rec_call ctxt t
    1.64        | massage_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t;
    1.65    in
    1.66      massage_call