diff -r 2e608fa6c404 -r 530e7a33b3dd src/Pure/search.ML
--- a/src/Pure/search.ML	Tue Jun 20 11:53:35 2000 +0200
+++ b/src/Pure/search.ML	Tue Jun 20 11:54:07 2000 +0200
@@ -37,6 +37,23 @@
   val QUIET_BREADTH_FIRST	: (thm -> bool) -> tactic -> tactic
   end;
 
+
+(** Instantiation of leftist heaps for best-first search **)
+
+(*Termless makes the ordering total, allowing duplicates to be found*)
+structure MeasureThm : ORDERED =
+struct
+  type T = int * thm
+  fun eq ((m,th):T, (m',th')) = (m=m' andalso eq_thm(th,th'))
+  fun lt ((m,th):T, (m',th')) = 
+          (m<m' orelse 
+	   m=m' andalso Term.termless (#prop(rep_thm th), #prop(rep_thm th')))
+  fun leq (mth, mth') = not (lt (mth',mth))
+end;
+
+structure MeasureThmHeap = LeftistHeap(MeasureThm);
+
+
 structure Search : SEARCH = 
 struct
 
@@ -184,18 +201,16 @@
 
 val trace_BEST_FIRST = ref false;
 
-(*Insertion into priority queue of states *)
-fun insert (nth: int*thm, []) = [nth]
-  | insert ((m,th), (n,th')::nths) = 
-      if  n<m then (n,th') :: insert ((m,th), nths)
-      else if  n=m andalso eq_thm(th,th')
-              then (n,th')::nths
-              else (m,th)::(n,th')::nths;
-
 (*For creating output sequence*)
 fun some_of_list []     = None
   | 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 MeasureThmHeap.isEmpty heap then heap
+      else if eq_thm (prf, #2 (MeasureThmHeap.findMin heap))
+      then deleteAllMin prf (MeasureThmHeap.deleteMin 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).
@@ -203,19 +218,22 @@
 fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 = 
   let val tac = tracify trace_BEST_FIRST tac1
       fun pairsize th = (sizef th, th);
-      fun bfs (news,nprfs) =
+      fun bfs (news,nprf_heap) =
 	   (case  partition satp news  of
-		([],nonsats) => next(foldr insert
-					(map pairsize nonsats, nprfs)) 
+		([],nonsats) => next(foldr MeasureThmHeap.insert
+					(map pairsize nonsats, nprf_heap)) 
 	      | (sats,_)  => some_of_list sats)
-      and next [] = None
-        | next ((n,prf)::nprfs) =
-	    (if !trace_BEST_FIRST 
-	       then writeln("state size = " ^ string_of_int n ^ 
-		         "  queue length =" ^ string_of_int (length nprfs))  
+      and next nprf_heap =
+            if MeasureThmHeap.isEmpty nprf_heap then None
+	    else 
+	    let val (n,prf) = MeasureThmHeap.findMin nprf_heap
+	    in if !trace_BEST_FIRST 
+	       then writeln("state size = " ^ string_of_int n)  
                else ();
-	     bfs (Seq.list_of (tac prf), nprfs))
-      fun btac st = bfs (Seq.list_of (tac0 st),  [])
+	       bfs (Seq.list_of (tac prf), 
+		    deleteAllMin prf (MeasureThmHeap.deleteMin nprf_heap))
+            end
+      fun btac st = bfs (Seq.list_of (tac0 st),  MeasureThmHeap.empty)
   in traced_tac btac end;
 
 (*Ordinary best-first search, with no initial tactic*)