src/HOL/Nominal/nominal_primrec.ML
changeset 33037 b22e44496dc2
parent 32196 bda40fb76a65
child 33038 8f9594c31de4
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -228,7 +228,7 @@
     1.4        (case Symtab.lookup dt_info tname of
     1.5            NONE => primrec_err (quote tname ^ " is not a nominal datatype")
     1.6          | SOME dt =>
     1.7 -            if tnames' subset (map (#1 o snd) (#descr dt)) then
     1.8 +            if gen_subset (op =) (tnames', map (#1 o snd) (#descr dt)) then
     1.9                (tname, dt)::(find_dts dt_info tnames' tnames)
    1.10              else find_dts dt_info tnames' tnames);
    1.11  
    1.12 @@ -251,7 +251,7 @@
    1.13      val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
    1.14        map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) eqns
    1.15      val _ =
    1.16 -      (if forall (curry eq_set lsrs) lsrss andalso forall
    1.17 +      (if forall (curry (gen_eq_set (op =)) lsrs) lsrss andalso forall
    1.18           (fn (_, (_, _, (_, (ls, _, rs, _, _)) :: eqns)) =>
    1.19                 forall (fn (_, (ls', _, rs', _, _)) =>
    1.20                   ls = ls' andalso rs = rs') eqns