changeset 33037 | b22e44496dc2 |
parent 32863 | 5e8cef567042 |
child 33038 | 8f9594c31de4 |
--- a/src/HOL/Tools/old_primrec.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/HOL/Tools/old_primrec.ML Tue Oct 20 16:13:01 2009 +0200 @@ -226,7 +226,7 @@ (case Symtab.lookup dt_info tname of NONE => primrec_err (quote tname ^ " is not a 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);