| changeset 59058 | a78612c67ec0 |
| parent 57942 | e5bec882fdd0 |
| child 59883 | 12a89103cae6 |
--- a/src/Pure/facts.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/facts.ML Wed Nov 26 20:05:34 2014 +0100 @@ -206,7 +206,7 @@ (* indexed props *) -val prop_ord = Term_Ord.term_ord o pairself Thm.full_prop_of; +val prop_ord = Term_Ord.term_ord o apply2 Thm.full_prop_of; fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props); fun could_unify (Facts {props, ...}) = Net.unify_term props;