| changeset 35408 | b48ab741683b |
| parent 33163 | 351fc13613f2 |
| child 42358 | b47d41d9f4b5 |
--- a/src/Pure/facts.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Pure/facts.ML Sat Feb 27 23:13:01 2010 +0100 @@ -171,7 +171,7 @@ (* indexed props *) -val prop_ord = TermOrd.term_ord o pairself Thm.full_prop_of; +val prop_ord = Term_Ord.term_ord o pairself Thm.full_prop_of; fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props); fun could_unify (Facts {props, ...}) = Net.unify_term props;