renamed functor HeapFun to Heap;
authorwenzelm
Thu Oct 15 11:12:09 2009 +0200 (2009-10-15)
changeset 329391b5a401c78cb
parent 32938 63a364ed3f8d
child 32940 51d450f278ce
renamed functor HeapFun to Heap;
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/Pure/General/heap.ML
src/Pure/search.ML
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Oct 15 10:59:10 2009 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Oct 15 11:12:09 2009 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4  
     1.5  (* data structures over threads *)
     1.6  
     1.7 -structure Thread_Heap = HeapFun
     1.8 +structure Thread_Heap = Heap
     1.9  (
    1.10    type elem = Time.time * Thread.thread;
    1.11    fun ord ((a, _), (b, _)) = Time.compare (a, b);
     2.1 --- a/src/Pure/General/heap.ML	Thu Oct 15 10:59:10 2009 +0200
     2.2 +++ b/src/Pure/General/heap.ML	Thu Oct 15 11:12:09 2009 +0200
     2.3 @@ -20,7 +20,7 @@
     2.4    val upto: elem -> T -> elem list * T
     2.5  end;
     2.6  
     2.7 -functor HeapFun(type elem val ord: elem * elem -> order): HEAP =
     2.8 +functor Heap(type elem val ord: elem * elem -> order): HEAP =
     2.9  struct
    2.10  
    2.11  
     3.1 --- a/src/Pure/search.ML	Thu Oct 15 10:59:10 2009 +0200
     3.2 +++ b/src/Pure/search.ML	Thu Oct 15 11:12:09 2009 +0200
     3.3 @@ -41,8 +41,11 @@
     3.4  (** Instantiation of heaps for best-first search **)
     3.5  
     3.6  (*total ordering on theorems, allowing duplicates to be found*)
     3.7 -structure ThmHeap = HeapFun(type elem = int * thm
     3.8 -  val ord = prod_ord int_ord (TermOrd.term_ord o pairself Thm.prop_of));
     3.9 +structure ThmHeap = Heap
    3.10 +(
    3.11 +  type elem = int * thm;
    3.12 +  val ord = prod_ord int_ord (TermOrd.term_ord o pairself Thm.prop_of);
    3.13 +);
    3.14  
    3.15  
    3.16  structure Search : SEARCH =