# HG changeset patch
# User wenzelm
# Date 1152613018 -7200
# Node ID da82b545d2de904bbea63a5fcba1424b9073d2cf
# Parent  c4710df2c953fc7cf585957d3f980fd4d170b205
removed obsolete mem_term;

diff -r c4710df2c953 -r da82b545d2de src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Tue Jul 11 12:16:57 2006 +0200
+++ b/src/HOL/Tools/meson.ML	Tue Jul 11 12:16:58 2006 +0200
@@ -122,7 +122,7 @@
   let val (poslits,neglits) = signed_lits th
   in  exists taut_poslit poslits
       orelse
-      exists (fn t => mem_term (t, neglits)) (HOLogic.false_const :: poslits)
+      exists (member (op aconv) neglits) (HOLogic.false_const :: poslits)
   end
   handle TERM _ => false;	(*probably dest_Trueprop on a weird theorem*)		      
 
diff -r c4710df2c953 -r da82b545d2de src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Tue Jul 11 12:16:57 2006 +0200
+++ b/src/HOL/Tools/refute.ML	Tue Jul 11 12:16:58 2006 +0200
@@ -491,7 +491,7 @@
 							end) class_axioms
 						(* Term.term list * (string * Term.term) list -> Term.term list *)
 						fun collect_axiom (axs, (axname, ax)) =
-							if mem_term (ax, axs) then
+							if member (op aconv) axs ax then
 								axs
 							else (
 								immediate_output (" " ^ axname);
@@ -561,7 +561,7 @@
 					| NONE =>
 						(case get_typedefn axioms of
 						  SOME (axname, ax) => 
-							if mem_term (ax, axs) then
+							if member (op aconv) axs ax then
 								(* only collect relevant type axioms for the argument types *)
 								Library.foldl collect_type_axioms (axs, Ts)
 							else
@@ -592,7 +592,7 @@
 				let
 					val ax = specialize_type (("The", T), (the o AList.lookup (op =) axioms) "HOL.the_eq_trivial")
 				in
-					if mem_term (ax, axs) then
+					if member (op aconv) axs ax then
 						collect_type_axioms (axs, T)
 					else
 						(immediate_output " HOL.the_eq_trivial";
@@ -603,7 +603,7 @@
 					val ax = specialize_type (("Hilbert_Choice.Eps", T),
                       (the o AList.lookup (op =) axioms) "Hilbert_Choice.someI")
 				in
-					if mem_term (ax, axs) then
+					if member (op aconv) axs ax then
 						collect_type_axioms (axs, T)
 					else
 						(immediate_output " Hilbert_Choice.someI";
@@ -689,13 +689,13 @@
 							val ofclass_ax = (SOME (specialize_type ((s, T), inclass)) handle Type.TYPE_MATCH => NONE)
 							val intro_ax   = (Option.map (fn t => specialize_type ((s, T), t))
 								(AList.lookup (op =) axioms (class ^ ".intro")) handle Type.TYPE_MATCH => NONE)
-							val axs'       = (case ofclass_ax of NONE => axs | SOME ax => if mem_term (ax, axs) then
+							val axs'       = (case ofclass_ax of NONE => axs | SOME ax => if member (op aconv) axs ax then
 									(* collect relevant type axioms *)
 									collect_type_axioms (axs, T)
 								else
 									(immediate_output (" " ^ Sign.string_of_term (sign_of thy) ax);
 									collect_term_axioms (ax :: axs, ax)))
-							val axs''      = (case intro_ax of NONE => axs' | SOME ax => if mem_term (ax, axs') then
+							val axs''      = (case intro_ax of NONE => axs' | SOME ax => if member (op aconv) axs' ax then
 									(* collect relevant type axioms *)
 									collect_type_axioms (axs', T)
 								else
@@ -713,7 +713,7 @@
 					else (
 						case get_defn axioms of
 						  SOME (axname, ax) => 
-							if mem_term (ax, axs) then
+							if member (op aconv) axs ax then
 								(* collect relevant type axioms *)
 								collect_type_axioms (axs, T)
 							else