# HG changeset patch
# User berghofe
# Date 1179479523 -7200
# Node ID c46abff9a7a081fbbf246e16b9f4810aeec59e19
# Parent  914a1de067b6e77306332dfdb20d9a7e836bb102
Fixed bug in subst causing primrec functions returning functions
to be rejected.

diff -r 914a1de067b6 -r c46abff9a7a0 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Fri May 18 09:16:57 2007 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Fri May 18 11:12:03 2007 +0200
@@ -116,11 +116,14 @@
                 val (x', rs) = (hd rest, tl rest)
                   handle Empty => raise RecError ("not enough arguments\
                    \ in recursive application\nof function " ^ quote fname' ^ " on rhs");
-                val _ = (case eqns of
+                val rs' = (case eqns of
                     (_, (ls', _, rs', _, _)) :: _ =>
-                      if ls = map Free ls' andalso rs = map Free rs' then ()
-                      else raise RecError param_err
-                  | _ => ());
+                      let val (rs1, rs2) = chop (length rs') rs
+                      in
+                        if ls = map Free ls' andalso rs1 = map Free rs' then rs2
+                        else raise RecError param_err
+                      end
+                  | _ => raise RecError ("no equations for " ^ quote fname'));
                 val (x, xs) = strip_comb x'
               in case AList.lookup (op =) subs x
                of NONE =>
@@ -129,7 +132,7 @@
                     |-> (fn ts' => pair (list_comb (f, ts')))
                 | SOME (i', y) =>
                     fs
-                    |> fold_map (subst subs) xs
+                    |> fold_map (subst subs) (xs @ rs')
                     ||> process_fun thy descr rec_eqns (i', fnameT')
                     |-> (fn ts' => pair (list_comb (y, ts')))
               end