diff -r 612ee826a409 -r 0d5a171db2f0 src/Pure/search.ML
--- a/src/Pure/search.ML	Sun Jul 23 12:02:22 2000 +0200
+++ b/src/Pure/search.ML	Sun Jul 23 12:04:56 2000 +0200
@@ -38,20 +38,13 @@
   end;
 
 
-(** Instantiation of leftist heaps for best-first search **)
+(** Instantiation of 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);
+(*total ordering on theorems, allowing duplicates to be found*)
+structure ThmHeap =
+  HeapFun (type elem = int * thm
+    val ord = Library.prod_ord Library.int_ord
+      (Term.term_ord o Library.pairself (#prop o Thm.rep_thm)));
 
 
 structure Search : SEARCH = 
@@ -207,9 +200,9 @@
 
 (*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)
+      if ThmHeap.is_empty heap then heap
+      else if 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)
@@ -220,20 +213,20 @@
       fun pairsize th = (sizef th, th);
       fun bfs (news,nprf_heap) =
 	   (case  partition satp news  of
-		([],nonsats) => next(foldr MeasureThmHeap.insert
+		([],nonsats) => next(foldr ThmHeap.insert
 					(map pairsize nonsats, nprf_heap)) 
 	      | (sats,_)  => some_of_list sats)
       and next nprf_heap =
-            if MeasureThmHeap.isEmpty nprf_heap then None
+            if ThmHeap.is_empty nprf_heap then None
 	    else 
-	    let val (n,prf) = MeasureThmHeap.findMin nprf_heap
+	    let val (n,prf) = ThmHeap.min nprf_heap
 	    in if !trace_BEST_FIRST 
 	       then writeln("state size = " ^ string_of_int n)  
                else ();
 	       bfs (Seq.list_of (tac prf), 
-		    deleteAllMin prf (MeasureThmHeap.deleteMin nprf_heap))
+		    deleteAllMin prf (ThmHeap.delete_min nprf_heap))
             end
-      fun btac st = bfs (Seq.list_of (tac0 st),  MeasureThmHeap.empty)
+      fun btac st = bfs (Seq.list_of (tac0 st), ThmHeap.empty)
   in traced_tac btac end;
 
 (*Ordinary best-first search, with no initial tactic*)