renamed functor HeapFun to Heap;

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Oct 15 10:59:10 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Oct 15 11:12:09 2009 +0200
@@ -69,7 +69,7 @@
 
 (* data structures over threads *)
 
-structure Thread_Heap = HeapFun
+structure Thread_Heap = Heap
 (
   type elem = Time.time * Thread.thread;
   fun ord ((a, _), (b, _)) = Time.compare (a, b);

--- a/src/Pure/General/heap.ML	Thu Oct 15 10:59:10 2009 +0200
+++ b/src/Pure/General/heap.ML	Thu Oct 15 11:12:09 2009 +0200
@@ -20,7 +20,7 @@
   val upto: elem -> T -> elem list * T
 end;
 
-functor HeapFun(type elem val ord: elem * elem -> order): HEAP =
+functor Heap(type elem val ord: elem * elem -> order): HEAP =
 struct
 
 

--- a/src/Pure/search.ML	Thu Oct 15 10:59:10 2009 +0200
+++ b/src/Pure/search.ML	Thu Oct 15 11:12:09 2009 +0200
@@ -41,8 +41,11 @@
 (** Instantiation of heaps for best-first search **)
 
 (*total ordering on theorems, allowing duplicates to be found*)
-structure ThmHeap = HeapFun(type elem = int * thm
-  val ord = prod_ord int_ord (TermOrd.term_ord o pairself Thm.prop_of));
+structure ThmHeap = Heap
+(
+  type elem = int * thm;
+  val ord = prod_ord int_ord (TermOrd.term_ord o pairself Thm.prop_of);
+);
 
 
 structure Search : SEARCH =