1.1 --- a/src/HOL/Tools/meson.ML	Tue Jun 13 23:41:34 2006 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Tue Jun 13 23:41:37 2006 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4  (*raises exception if no rules apply -- unlike RL*)
     1.5  fun tryres (th, rls) = 
     1.6    let fun tryall [] = raise THM("tryres", 0, th::rls)
     1.7 -        | tryall (rl::rls) = (resolve1(th,rl) handle Option => tryall rls)
     1.8 +        | tryall (rl::rls) = (resolve1(th,rl) handle Option.Option => tryall rls)
     1.9    in  tryall rls  end;
    1.10    
    1.11  (*Permits forward proof from rules that discharge assumptions*)
    1.12 @@ -84,7 +84,7 @@
    1.13  
    1.14  (*Are any of the constants in "bs" present in the term?*)
    1.15  fun has_consts bs =
    1.16 -  let fun has (Const(a,_)) = a mem bs
    1.17 +  let fun has (Const(a,_)) = member (op =) bs a
    1.18  	| has (Const ("Hilbert_Choice.Eps",_) $ _) = false
    1.19  		     (*ignore constants within @-terms*)
    1.20  	| has (f$u) = has f orelse has u
    1.21 @@ -266,7 +266,7 @@
    1.22  (*Is the string the name of a connective? It doesn't matter if this list is
    1.23    incomplete, since when actually called, the only connectives likely to
    1.24    remain are & | Not.*)  
    1.25 -fun is_conn c = c mem_string
    1.26 +val is_conn = member (op =)
    1.27      ["Trueprop", "HOL.tag", "op &", "op |", "op -->", "op =", "Not", 
    1.28       "All", "Ex", "Ball", "Bex"];
    1.29  
    1.30 @@ -336,7 +336,7 @@
    1.31    | has_reps [_] = false
    1.32    | has_reps [t,u] = (t aconv u)
    1.33    | has_reps ts = (Library.foldl ins_term (Net.empty, ts);  false)
    1.34 -		  handle INSERT => true;
    1.35 +		  handle Net.INSERT => true;
    1.36  
    1.37  (*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
    1.38  fun TRYING_eq_assume_tac 0 st = Seq.single st