--- 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 =