1.1 --- a/src/Tools/isac/ME/rewtools.sml	Thu Aug 19 12:08:42 2010 +0200
     1.2 +++ b/src/Tools/isac/ME/rewtools.sml	Thu Aug 19 15:02:06 2010 +0200
     1.3 @@ -244,12 +244,10 @@
     1.4  				(rule2str r1)^"' '"^(rule2str r2)^"'");
     1.5  fun distinct_Thm r = gen_distinct eq_Thm r;
     1.6  
     1.7 -fun eq_Thms thmIDs thm = ((id_of_thm thm) mem thmIDs)
     1.8 +fun eq_Thms thmIDs thm = (member op = (id_of_thm thm) thmIDs)
     1.9      handle _ => false;
    1.10  
    1.11  
    1.12 -
    1.13 -
    1.14  (***. context to thy concerning rewriting .***)
    1.15  
    1.16  (*.create the unique handles and filenames for the theory-data.*)
    1.17 @@ -371,7 +369,7 @@
    1.18     val (str, (_, thy)) = ("real_diff_minus", ("Poly.thy", Poly.thy));
    1.19     *)
    1.20  fun thy_contains_thm (str:xstring) (_, thy) = 
    1.21 -    str mem (map (strip_thy o fst) (thms_of thy));
    1.22 +    member str (map (strip_thy o fst) (thms_of thy));
    1.23  (* val (thy', str) = ("Isac.thy", "real_mult_minus1");
    1.24     val (thy', str) = ("PolyMinus.thy", "klammer_minus_plus");
    1.25     *)
    1.26 @@ -723,7 +721,7 @@
    1.27      let val guh' = explode guh
    1.28  	val part = implode (take_fromto 1 4 guh')
    1.29  	val isa = implode (take_fromto 5 9 guh')
    1.30 -    in if not (part mem ["exp_", "thy_", "pbl_", "met_"])
    1.31 +    in if not (member op = part ["exp_", "thy_", "pbl_", "met_"])
    1.32         then raise error ("guh '"^guh^"' does not begin with \
    1.33  				     \exp_ | thy_ | pbl_ | met_")
    1.34         else let val chap = case isa of