| changeset 35408 | b48ab741683b |
| parent 33380 | cd6023a9a922 |
| child 38802 | a925c0ee42f7 |
--- a/src/Pure/search.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Pure/search.ML Sat Feb 27 23:13:01 2010 +0100 @@ -197,7 +197,7 @@ structure Thm_Heap = Heap ( type elem = int * thm; - val ord = prod_ord int_ord (TermOrd.term_ord o pairself Thm.prop_of); + val ord = prod_ord int_ord (Term_Ord.term_ord o pairself Thm.prop_of); ); val trace_BEST_FIRST = Unsynchronized.ref false;