1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 20 19:20:08 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 20 19:23:28 2013 +0200
     1.3 @@ -168,7 +168,7 @@
     1.4      subst (SOME ~1)
     1.5    end;
     1.6  
     1.7 -fun subst_rec_calls lthy get_ctr_pos has_call ctr_args mutual_calls nested_calls t =
     1.8 +fun subst_rec_calls lthy get_ctr_pos has_call ctr_args mutual_calls nested_calls =
     1.9    let
    1.10      fun try_nested_rec bound_Ts y t =
    1.11        AList.lookup (op =) nested_calls y
    1.12 @@ -176,9 +176,12 @@
    1.13          massage_nested_rec_call lthy has_call (rewrite_map_arg get_ctr_pos) bound_Ts y y' t);
    1.14  
    1.15      fun subst bound_Ts (t as g' $ y) =
    1.16 -        let val y_head = head_of y in
    1.17 +        let
    1.18 +          fun subst_rec () = subst bound_Ts g' $ subst bound_Ts y;
    1.19 +          val y_head = head_of y;
    1.20 +        in
    1.21            if not (member (op =) ctr_args y_head) then
    1.22 -            subst bound_Ts g' $ subst bound_Ts y
    1.23 +            subst_rec ()
    1.24            else
    1.25              (case try_nested_rec bound_Ts y_head t of
    1.26                SOME t' => t'
    1.27 @@ -190,16 +193,21 @@
    1.28                     primrec_error_eqn "too few arguments in recursive call" t;
    1.29                     (case AList.lookup (op =) mutual_calls y of
    1.30                       SOME y' => list_comb (y', g_args)
    1.31 -                   | NONE => t))
    1.32 -                | NONE => t)
    1.33 +                   | NONE => subst_rec ()))
    1.34 +                | NONE => subst_rec ())
    1.35                end)
    1.36          end
    1.37        | subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)
    1.38        | subst _ t = t
    1.39 +
    1.40 +    fun subst' t =
    1.41 +      if has_call t then
    1.42 +        (* FIXME detect this case earlier? *)
    1.43 +        primrec_error_eqn "recursive call not directly applied to constructor argument" t
    1.44 +      else
    1.45 +        try_nested_rec [] (head_of t) t |> the_default t
    1.46    in
    1.47 -    subst [] t
    1.48 -    |> tap (fn u => has_call u andalso (* FIXME detect this case earlier *)
    1.49 -      primrec_error_eqn "recursive call not directly applied to constructor argument" t)
    1.50 +    subst' o subst []
    1.51    end;
    1.52  
    1.53  fun build_rec_arg lthy (funs_data : eqn_data list list) has_call (ctr_spec : rec_ctr_spec)

     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Sun Oct 20 19:20:08 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Sun Oct 20 19:23:28 2013 +0200
     2.3 @@ -274,17 +274,20 @@
     2.4          handle AINT_NO_MAP _ => massage_mutual_fun U T t;
     2.5  
     2.6      fun massage_call (t as t1 $ t2) =
     2.7 -        if t2 = y then
     2.8 -          massage_map yU yT (elim_y t1) $ y'
     2.9 -          handle AINT_NO_MAP t' => invalid_map ctxt t'
    2.10 +        if has_call t then
    2.11 +          if t2 = y then
    2.12 +            massage_map yU yT (elim_y t1) $ y'
    2.13 +            handle AINT_NO_MAP t' => invalid_map ctxt t'
    2.14 +          else
    2.15 +            let val (g, xs) = Term.strip_comb t2 in
    2.16 +              if g = y then
    2.17 +                if exists has_call xs then unexpected_rec_call ctxt t2
    2.18 +                else Term.list_comb (massage_call (mk_compN bound_Ts (length xs) (t1, y)), xs)
    2.19 +              else
    2.20 +                ill_formed_rec_call ctxt t
    2.21 +            end
    2.22          else
    2.23 -          let val (g, xs) = Term.strip_comb t2 in
    2.24 -            if g = y then
    2.25 -              if exists has_call xs then unexpected_rec_call ctxt t2
    2.26 -              else Term.list_comb (massage_call (mk_compN bound_Ts (length xs) (t1, y)), xs)
    2.27 -            else
    2.28 -              ill_formed_rec_call ctxt t
    2.29 -          end
    2.30 +          elim_y t
    2.31        | massage_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t;
    2.32    in
    2.33      massage_call