diff -r cc4b2b882e4c -r 7405ce9d4f25 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Tue Jun 13 23:41:34 2006 +0200
+++ b/src/HOL/Tools/meson.ML	Tue Jun 13 23:41:37 2006 +0200
@@ -72,7 +72,7 @@
 (*raises exception if no rules apply -- unlike RL*)
 fun tryres (th, rls) = 
   let fun tryall [] = raise THM("tryres", 0, th::rls)
-        | tryall (rl::rls) = (resolve1(th,rl) handle Option => tryall rls)
+        | tryall (rl::rls) = (resolve1(th,rl) handle Option.Option => tryall rls)
   in  tryall rls  end;
   
 (*Permits forward proof from rules that discharge assumptions*)
@@ -84,7 +84,7 @@
 
 (*Are any of the constants in "bs" present in the term?*)
 fun has_consts bs =
-  let fun has (Const(a,_)) = a mem bs
+  let fun has (Const(a,_)) = member (op =) bs a
 	| has (Const ("Hilbert_Choice.Eps",_) $ _) = false
 		     (*ignore constants within @-terms*)
 	| has (f$u) = has f orelse has u
@@ -266,7 +266,7 @@
 (*Is the string the name of a connective? It doesn't matter if this list is
   incomplete, since when actually called, the only connectives likely to
   remain are & | Not.*)  
-fun is_conn c = c mem_string
+val is_conn = member (op =)
     ["Trueprop", "HOL.tag", "op &", "op |", "op -->", "op =", "Not", 
      "All", "Ex", "Ball", "Bex"];
 
@@ -336,7 +336,7 @@
   | has_reps [_] = false
   | has_reps [t,u] = (t aconv u)
   | has_reps ts = (Library.foldl ins_term (Net.empty, ts);  false)
-		  handle INSERT => true;
+		  handle Net.INSERT => true;
 
 (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
 fun TRYING_eq_assume_tac 0 st = Seq.single st