diff -r 862f35fdb091 -r f2b8d1b3fcc2 src/Tools/isac/ME/rewtools.sml
--- a/src/Tools/isac/ME/rewtools.sml	Thu Aug 19 12:08:42 2010 +0200
+++ b/src/Tools/isac/ME/rewtools.sml	Thu Aug 19 15:02:06 2010 +0200
@@ -244,12 +244,10 @@
 				(rule2str r1)^"' '"^(rule2str r2)^"'");
 fun distinct_Thm r = gen_distinct eq_Thm r;
 
-fun eq_Thms thmIDs thm = ((id_of_thm thm) mem thmIDs)
+fun eq_Thms thmIDs thm = (member op = (id_of_thm thm) thmIDs)
     handle _ => false;
 
 
-
-
 (***. context to thy concerning rewriting .***)
 
 (*.create the unique handles and filenames for the theory-data.*)
@@ -371,7 +369,7 @@
    val (str, (_, thy)) = ("real_diff_minus", ("Poly.thy", Poly.thy));
    *)
 fun thy_contains_thm (str:xstring) (_, thy) = 
-    str mem (map (strip_thy o fst) (thms_of thy));
+    member str (map (strip_thy o fst) (thms_of thy));
 (* val (thy', str) = ("Isac.thy", "real_mult_minus1");
    val (thy', str) = ("PolyMinus.thy", "klammer_minus_plus");
    *)
@@ -723,7 +721,7 @@
     let val guh' = explode guh
 	val part = implode (take_fromto 1 4 guh')
 	val isa = implode (take_fromto 5 9 guh')
-    in if not (part mem ["exp_", "thy_", "pbl_", "met_"])
+    in if not (member op = part ["exp_", "thy_", "pbl_", "met_"])
        then raise error ("guh '"^guh^"' does not begin with \
 				     \exp_ | thy_ | pbl_ | met_")
        else let val chap = case isa of