src/HOL/Nominal/nominal_primrec.ML
changeset 22330 00ca68f5ce29
parent 22101 6d13239d5f52
child 22434 081a62852313
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Fri Feb 16 11:01:16 2007 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Feb 16 19:19:19 2007 +0100
     1.3 @@ -243,7 +243,7 @@
     1.4                 forall (fn (_, (ls', _, rs', _, _)) =>
     1.5                   ls = ls' andalso rs = rs') eqns
     1.6             | _ => true) rec_eqns
     1.7 -       then () else raise RecError param_err);
     1.8 +       then () else primrec_err param_err);
     1.9      val tnames = distinct (op =) (map (#1 o snd) rec_eqns);
    1.10      val dts = find_dts dt_info tnames tnames;
    1.11      val main_fns =