src/Pure/thm.ML

--- a/src/Pure/thm.ML	Thu Sep 09 14:50:26 2021 +0200
+++ b/src/Pure/thm.ML	Thu Sep 09 15:45:27 2021 +0200
@@ -41,6 +41,8 @@
   val global_cterm_of: theory -> term -> cterm
   val cterm_of: Proof.context -> term -> cterm
   val renamed_term: term -> cterm -> cterm
+  val fast_term_ord: cterm ord
+  val term_ord: cterm ord
   val dest_comb: cterm -> cterm * cterm
   val dest_fun: cterm -> cterm
   val dest_arg: cterm -> cterm
@@ -82,6 +84,7 @@
   val cconcl_of: thm -> cterm
   val cprems_of: thm -> cterm list
   val chyps_of: thm -> cterm list
+  val thm_ord: thm ord
   exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option
   val theory_of_cterm: cterm -> theory
   val theory_of_thm: thm -> theory
@@ -269,6 +272,9 @@
   if t aconv t' then Cterm {cert = cert, t = t', T = T, maxidx = maxidx, sorts = sorts}
   else raise TERM ("renamed_term: terms disagree", [t, t']);
 
+val fast_term_ord = Term_Ord.fast_term_ord o apply2 term_of;
+val term_ord = Term_Ord.term_ord o apply2 term_of;
+
 
 (* destructors *)
 
@@ -518,6 +524,15 @@
   map (fn t => Cterm {cert = cert, maxidx = ~1, T = propT, sorts = shyps, t = t}) hyps;
 
 
+(* thm order: ignores theory context! *)
+
+val thm_ord =
+  Term_Ord.fast_term_ord o apply2 prop_of
+  ||| list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) o apply2 tpairs_of
+  ||| list_ord Term_Ord.fast_term_ord o apply2 hyps_of
+  ||| list_ord Term_Ord.sort_ord o apply2 shyps_of;
+
+
 (* implicit theory context *)
 
 exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option;