src/Pure/Tools/class_package.ML
changeset 19300 7689f81f8996
parent 19293 a67b9916c58e
child 19340 a4fe025ecd90
--- a/src/Pure/Tools/class_package.ML	Tue Mar 21 12:18:06 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Tue Mar 21 12:18:07 2006 +0100
@@ -521,11 +521,11 @@
             andalso Sign.typ_instance thy (ty1', ty2')
             andalso Sign.typ_instance thy (ty2', ty1')
           end;
-        val _ = case fold (remove eq_c) c_req c_given
+        val _ = case subtract eq_c c_req c_given
          of [] => ()
           | cs => error ("superfluous definition(s) given for "
                     ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);
-        val _ = case fold (remove eq_c) c_given c_req
+        val _ = case subtract eq_c c_given c_req
          of [] => ()
           | cs => error ("no definition(s) given for "
                     ^ (commas o map (fn (c, ty) => quote (c ^ "::" ^ Sign.string_of_typ thy ty))) cs);