1.1 --- a/src/HOL/Tools/primrec_package.ML	Fri Jun 20 21:00:22 2008 +0200
     1.2 +++ b/src/HOL/Tools/primrec_package.ML	Fri Jun 20 21:00:25 2008 +0200
     1.3 @@ -106,10 +106,12 @@
     1.4                let
     1.5                  val (fname', _) = dest_Free f;
     1.6                  val (_, rpos, _) = the (AList.lookup (op =) eqns fname');
     1.7 -                val (ls, x' :: rs) = chop rpos ts
     1.8 -                  handle Empty => primrec_error ("not enough arguments\
     1.9 -                   \ in recursive application\nof function " ^ quote fname' ^ " on rhs");
    1.10 -                val (x, xs) = strip_comb x'
    1.11 +                val (ls, rs) = chop rpos ts
    1.12 +                val (x', rs') = case rs
    1.13 +                 of x' :: rs => (x', rs)
    1.14 +                  | [] => primrec_error ("not enough arguments in recursive application\n"
    1.15 +                      ^ "of function " ^ quote fname' ^ " on rhs");
    1.16 +                val (x, xs) = strip_comb x';
    1.17                in case AList.lookup (op =) subs x
    1.18                 of NONE =>
    1.19                      fs
    1.20 @@ -117,7 +119,7 @@
    1.21                      |-> (fn ts' => pair (list_comb (f, ts')))
    1.22                  | SOME (i', y) =>
    1.23                      fs
    1.24 -                    |> fold_map (subst subs) (xs @ ls @ rs)
    1.25 +                    |> fold_map (subst subs) (xs @ ls @ rs')
    1.26                      ||> process_fun descr eqns (i', fname')
    1.27                      |-> (fn ts' => pair (list_comb (y, ts')))
    1.28                end
    1.29 @@ -141,8 +143,8 @@
    1.30                val rargs = map fst recs;
    1.31                val subs = map (rpair dummyT o fst)
    1.32                  (rev (rename_wrt_term rhs rargs));
    1.33 -              val (rhs', (fnames'', fnss'')) = (subst (map2 (fn (x, y) => fn z =>
    1.34 -                (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss'))
    1.35 +              val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
    1.36 +                (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
    1.37                    handle PrimrecError (s, NONE) => primrec_error_eqn s eq
    1.38              in (fnames'', fnss'',
    1.39                  (list_abs_free (cargs' @ subs @ ls @ rs, rhs'))::fns)