# HG changeset patch
# User berghofe
# Date 1171649959 -3600
# Node ID 00ca68f5ce29ae8f0eab2c015f961296093fa18c
# Parent  e4325ce4e0c4ea11177eda352398c81f6a51ace5
Replaced "raise RecError" by "primrec_err" in function
gen_primrec_i to prevent error message from being suppressed.

diff -r e4325ce4e0c4 -r 00ca68f5ce29 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Fri Feb 16 11:01:16 2007 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Feb 16 19:19:19 2007 +0100
@@ -243,7 +243,7 @@
                forall (fn (_, (ls', _, rs', _, _)) =>
                  ls = ls' andalso rs = rs') eqns
            | _ => true) rec_eqns
-       then () else raise RecError param_err);
+       then () else primrec_err param_err);
     val tnames = distinct (op =) (map (#1 o snd) rec_eqns);
     val dts = find_dts dt_info tnames tnames;
     val main_fns =