# HG changeset patch
# User wenzelm
# Date 1255597929 -7200
# Node ID 1b5a401c78cb597268ddc1a317b06c3d17e27c0d
# Parent  63a364ed3f8d254ae939e3a914847e85688d314d
renamed functor HeapFun to Heap;

diff -r 63a364ed3f8d -r 1b5a401c78cb src/HOL/Tools/ATP_Manager/atp_manager.ML
--- 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);
diff -r 63a364ed3f8d -r 1b5a401c78cb src/Pure/General/heap.ML
--- 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
 
 
diff -r 63a364ed3f8d -r 1b5a401c78cb src/Pure/search.ML
--- 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 =