--- a/src/Pure/more_thm.ML Tue Aug 20 09:48:22 2019 +0200
+++ b/src/Pure/more_thm.ML Tue Aug 20 11:01:05 2019 +0200
@@ -40,9 +40,9 @@
val dest_equals_rhs: cterm -> cterm
val lhs_of: thm -> cterm
val rhs_of: thm -> cterm
- val fast_term_ord: cterm * cterm -> order
- val term_ord: cterm * cterm -> order
- val thm_ord: thm * thm -> order
+ val fast_term_ord: cterm ord
+ val term_ord: cterm ord
+ val thm_ord: thm ord
val cterm_cache: (cterm -> 'a) -> cterm -> 'a
val thm_cache: (thm -> 'a) -> thm -> 'a
val is_reflexive: thm -> bool