src/Pure/search.ML
changeset 18921 f47c46d7d654
parent 16179 fa7e70be26b0
child 19482 9f11af8f7ef9
     1.1 --- a/src/Pure/search.ML	Fri Feb 03 17:08:03 2006 +0100
     1.2 +++ b/src/Pure/search.ML	Fri Feb 03 23:12:28 2006 +0100
     1.3 @@ -63,7 +63,7 @@
     1.4  	  case Seq.pull q of
     1.5  	      NONE         => depth used qs
     1.6  	    | SOME(st,stq) => 
     1.7 -		if satp st andalso not (gen_mem eq_thm (st, used))
     1.8 +		if satp st andalso not (member eq_thm used st)
     1.9  		then SOME(st, Seq.make
    1.10  			         (fn()=> depth (st::used) (stq::qs)))
    1.11  		else depth used (tac st :: stq :: qs)