fixed bind error for malformed primrec specifications
authorhaftmann
Fri, 20 Jun 2008 21:00:25 +0200
changeset 27301 bf7d82193a2e
parent 27300 4cb3101d2bf7
child 27302 8d12ac6a3e1c
fixed bind error for malformed primrec specifications
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)