--- a/src/HOL/Nominal/nominal_primrec.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Tue Oct 20 16:13:01 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 tnames' subset (map (#1 o snd) (#descr dt)) then
+ if gen_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 eq_set lsrs) lsrss andalso forall
+ (if forall (curry (gen_eq_set (op =)) lsrs) lsrss andalso forall
(fn (_, (_, _, (_, (ls, _, rs, _, _)) :: eqns)) =>
forall (fn (_, (ls', _, rs', _, _)) =>
ls = ls' andalso rs = rs') eqns