--- a/src/HOL/Tools/primrec_package.ML Fri Jun 20 21:00:22 2008 +0200
+++ b/src/HOL/Tools/primrec_package.ML Fri Jun 20 21:00:25 2008 +0200
@@ -106,10 +106,12 @@
let
val (fname', _) = dest_Free f;
val (_, rpos, _) = the (AList.lookup (op =) eqns fname');
- val (ls, x' :: rs) = chop rpos ts
- handle Empty => primrec_error ("not enough arguments\
- \ in recursive application\nof function " ^ quote fname' ^ " on rhs");
- val (x, xs) = strip_comb x'
+ val (ls, rs) = chop rpos ts
+ val (x', rs') = case rs
+ of x' :: rs => (x', rs)
+ | [] => primrec_error ("not enough arguments in recursive application\n"
+ ^ "of function " ^ quote fname' ^ " on rhs");
+ val (x, xs) = strip_comb x';
in case AList.lookup (op =) subs x
of NONE =>
fs
@@ -117,7 +119,7 @@
|-> (fn ts' => pair (list_comb (f, ts')))
| SOME (i', y) =>
fs
- |> fold_map (subst subs) (xs @ ls @ rs)
+ |> fold_map (subst subs) (xs @ ls @ rs')
||> process_fun descr eqns (i', fname')
|-> (fn ts' => pair (list_comb (y, ts')))
end
@@ -141,8 +143,8 @@
val rargs = map fst recs;
val subs = map (rpair dummyT o fst)
(rev (rename_wrt_term rhs rargs));
- val (rhs', (fnames'', fnss'')) = (subst (map2 (fn (x, y) => fn z =>
- (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss'))
+ val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
+ (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
handle PrimrecError (s, NONE) => primrec_error_eqn s eq
in (fnames'', fnss'',
(list_abs_free (cargs' @ subs @ ls @ rs, rhs'))::fns)