--- a/src/Pure/more_thm.ML Wed Jan 31 21:05:47 2018 +0100
+++ b/src/Pure/more_thm.ML Thu Feb 01 13:55:10 2018 +0100
@@ -38,6 +38,8 @@
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 cterm_cache: (cterm -> 'a) -> cterm -> 'a
val thm_cache: (thm -> 'a) -> thm -> 'a
@@ -179,6 +181,12 @@
val rhs_of = dest_equals_rhs o Thm.cprop_of;
+(* certified term order *)
+
+val fast_term_ord = Term_Ord.fast_term_ord o apply2 Thm.term_of;
+val term_ord = Term_Ord.term_ord o apply2 Thm.term_of;
+
+
(* thm order: ignores theory context! *)
fun thm_ord ths =
@@ -198,7 +206,7 @@
(* tables and caches *)
-structure Ctermtab = Table(type key = cterm val ord = Term_Ord.fast_term_ord o apply2 Thm.term_of);
+structure Ctermtab = Table(type key = cterm val ord = fast_term_ord);
structure Thmtab = Table(type key = thm val ord = thm_ord);
fun cterm_cache f = Cache.create Ctermtab.empty Ctermtab.lookup Ctermtab.update f;