src/Pure/search.ML

      fun depth used [] = NONE
        | depth used (q::qs) =
 	  case Seq.pull q of
 	      NONE         => depth used qs
 	    | SOME(st,stq) => 
-		if satp st andalso not (member eq_thm used st)
+		if satp st andalso not (member Thm.eq_thm used st)
 		then SOME(st, Seq.make
 			         (fn()=> depth (st::used) (stq::qs)))
 		else depth used (tac st :: stq :: qs)
   in  traced_tac (fn st => depth [] [Seq.single st])  end;
 

   | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
 
 (*Check for and delete duplicate proof states*)
 fun deleteAllMin prf heap = 
       if ThmHeap.is_empty heap then heap
-      else if eq_thm (prf, #2 (ThmHeap.min heap))
+      else if Thm.eq_thm (prf, #2 (ThmHeap.min heap))
       then deleteAllMin prf (ThmHeap.delete_min heap)
       else heap;
 
 (*Best-first search for a state that satisfies satp (incl initial state)
   Function sizef estimates size of problem remaining (smaller means better).

 
 (*Insertion into priority queue of states, marked with level *)
 fun insert_with_level (lnth: int*int*thm, []) = [lnth]
   | insert_with_level ((l,m,th), (l',n,th')::nths) = 
       if  n<m then (l',n,th') :: insert_with_level ((l,m,th), nths)
-      else if  n=m andalso eq_thm(th,th')
+      else if  n=m andalso Thm.eq_thm(th,th')
               then (l',n,th')::nths
               else (l,m,th)::(l',n,th')::nths;
 
 (*For creating output sequence*)
 fun some_of_list []     = NONE