| changeset 59058 | a78612c67ec0 |
| parent 55171 | dc7a6f6be01b |
| child 59582 | 0fbed69ff081 |
--- a/src/Pure/search.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/search.ML Wed Nov 26 20:05:34 2014 +0100 @@ -194,7 +194,7 @@ structure Thm_Heap = Heap ( type elem = int * thm; - val ord = prod_ord int_ord (Term_Ord.term_ord o pairself Thm.prop_of); + val ord = prod_ord int_ord (Term_Ord.term_ord o apply2 Thm.prop_of); ); val trace_BEST_FIRST = Unsynchronized.ref false;