1.1 --- a/src/HOL/Tools/meson.ML	Tue Jul 11 12:16:57 2006 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Tue Jul 11 12:16:58 2006 +0200
     1.3 @@ -122,7 +122,7 @@
     1.4    let val (poslits,neglits) = signed_lits th
     1.5    in  exists taut_poslit poslits
     1.6        orelse
     1.7 -      exists (fn t => mem_term (t, neglits)) (HOLogic.false_const :: poslits)
     1.8 +      exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
     1.9    end
    1.10    handle TERM _ => false;	(*probably dest_Trueprop on a weird theorem*)		      
    1.11  

     2.1 --- a/src/HOL/Tools/refute.ML	Tue Jul 11 12:16:57 2006 +0200
     2.2 +++ b/src/HOL/Tools/refute.ML	Tue Jul 11 12:16:58 2006 +0200
     2.3 @@ -491,7 +491,7 @@
     2.4  							end) class_axioms
     2.5  						(* Term.term list * (string * Term.term) list -> Term.term list *)
     2.6  						fun collect_axiom (axs, (axname, ax)) =
     2.7 -							if mem_term (ax, axs) then
     2.8 +							if member (op aconv) axs ax then
     2.9  								axs
    2.10  							else (
    2.11  								immediate_output (" " ^ axname);
    2.12 @@ -561,7 +561,7 @@
    2.13  					| NONE =>
    2.14  						(case get_typedefn axioms of
    2.15  						  SOME (axname, ax) => 
    2.16 -							if mem_term (ax, axs) then
    2.17 +							if member (op aconv) axs ax then
    2.18  								(* only collect relevant type axioms for the argument types *)
    2.19  								Library.foldl collect_type_axioms (axs, Ts)
    2.20  							else
    2.21 @@ -592,7 +592,7 @@
    2.22  				let
    2.23  					val ax = specialize_type (("The", T), (the o AList.lookup (op =) axioms) "HOL.the_eq_trivial")
    2.24  				in
    2.25 -					if mem_term (ax, axs) then
    2.26 +					if member (op aconv) axs ax then
    2.27  						collect_type_axioms (axs, T)
    2.28  					else
    2.29  						(immediate_output " HOL.the_eq_trivial";
    2.30 @@ -603,7 +603,7 @@
    2.31  					val ax = specialize_type (("Hilbert_Choice.Eps", T),
    2.32                        (the o AList.lookup (op =) axioms) "Hilbert_Choice.someI")
    2.33  				in
    2.34 -					if mem_term (ax, axs) then
    2.35 +					if member (op aconv) axs ax then
    2.36  						collect_type_axioms (axs, T)
    2.37  					else
    2.38  						(immediate_output " Hilbert_Choice.someI";
    2.39 @@ -689,13 +689,13 @@
    2.40  							val ofclass_ax = (SOME (specialize_type ((s, T), inclass)) handle Type.TYPE_MATCH => NONE)
    2.41  							val intro_ax   = (Option.map (fn t => specialize_type ((s, T), t))
    2.42  								(AList.lookup (op =) axioms (class ^ ".intro")) handle Type.TYPE_MATCH => NONE)
    2.43 -							val axs'       = (case ofclass_ax of NONE => axs | SOME ax => if mem_term (ax, axs) then
    2.44 +							val axs'       = (case ofclass_ax of NONE => axs | SOME ax => if member (op aconv) axs ax then
    2.45  									(* collect relevant type axioms *)
    2.46  									collect_type_axioms (axs, T)
    2.47  								else
    2.48  									(immediate_output (" " ^ Sign.string_of_term (sign_of thy) ax);
    2.49  									collect_term_axioms (ax :: axs, ax)))
    2.50 -							val axs''      = (case intro_ax of NONE => axs' | SOME ax => if mem_term (ax, axs') then
    2.51 +							val axs''      = (case intro_ax of NONE => axs' | SOME ax => if member (op aconv) axs' ax then
    2.52  									(* collect relevant type axioms *)
    2.53  									collect_type_axioms (axs', T)
    2.54  								else
    2.55 @@ -713,7 +713,7 @@
    2.56  					else (
    2.57  						case get_defn axioms of
    2.58  						  SOME (axname, ax) => 
    2.59 -							if mem_term (ax, axs) then
    2.60 +							if member (op aconv) axs ax then
    2.61  								(* collect relevant type axioms *)
    2.62  								collect_type_axioms (axs, T)
    2.63  							else