# HG changeset patch
# User haftmann
# Date 1213988425 -7200
# Node ID bf7d82193a2e4191f36d005b1269f60d1cfb6634
# Parent  4cb3101d2bf779ba871acdffcc0944ae2c8ac75b
fixed bind error for malformed primrec specifications

diff -r 4cb3101d2bf7 -r bf7d82193a2e src/HOL/Tools/primrec_package.ML
--- 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)