--- a/src/HOL/Nominal/nominal_primrec.ML Tue Oct 20 16:13:01 2009 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Wed Oct 21 08:14:38 2009 +0200
@@ -228,7 +228,7 @@
(case Symtab.lookup dt_info tname of
NONE => primrec_err (quote tname ^ " is not a nominal datatype")
| SOME dt =>
- if gen_subset (op =) (tnames', map (#1 o snd) (#descr dt)) then
+ if subset (op =) (tnames', map (#1 o snd) (#descr dt)) then
(tname, dt)::(find_dts dt_info tnames' tnames)
else find_dts dt_info tnames' tnames);
@@ -251,7 +251,7 @@
val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) eqns
val _ =
- (if forall (curry (gen_eq_set (op =)) lsrs) lsrss andalso forall
+ (if forall (curry (eq_set (op =)) lsrs) lsrss andalso forall
(fn (_, (_, _, (_, (ls, _, rs, _, _)) :: eqns)) =>
forall (fn (_, (ls', _, rs', _, _)) =>
ls = ls' andalso rs = rs') eqns
@@ -276,7 +276,7 @@
val defs' = map (make_def lthy fixes fs) defs;
val names1 = map snd fnames;
val names2 = map fst eqns;
- val _ = if gen_eq_set (op =) (names1, names2) then ()
+ val _ = if eq_set (op =) (names1, names2) then ()
else primrec_err ("functions " ^ commas_quote names2 ^
"\nare not mutually recursive");
val (defs_thms, lthy') = lthy |>