src/Pure/search.ML

--- a/src/Pure/search.ML	Fri Feb 03 17:08:03 2006 +0100
+++ b/src/Pure/search.ML	Fri Feb 03 23:12:28 2006 +0100
@@ -63,7 +63,7 @@
 	  case Seq.pull q of
 	      NONE         => depth used qs
 	    | SOME(st,stq) => 
-		if satp st andalso not (gen_mem eq_thm (st, used))
+		if satp st andalso not (member eq_thm used st)
 		then SOME(st, Seq.make
 			         (fn()=> depth (st::used) (stq::qs)))
 		else depth used (tac st :: stq :: qs)