# HG changeset patch
# User wenzelm
# Date 1517489710 -3600
# Node ID 833d154ab189e1d07f8cdbbc22cc1b9ba937804e
# Parent  c46910a6bfce9419c0573ea09217d9bc2c301acf
clarified signature;

diff -r c46910a6bfce -r 833d154ab189 src/HOL/Analysis/normarith.ML
--- a/src/HOL/Analysis/normarith.ML	Wed Jan 31 21:05:47 2018 +0100
+++ b/src/HOL/Analysis/normarith.ML	Thu Feb 01 13:55:10 2018 +0100
@@ -375,7 +375,7 @@
 local
  val rawrule = fconv_rule (arg_conv (rewr_conv @{thm real_eq_0_iff_le_ge_0}))
  fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
- fun simple_cterm_ord t u = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS;
+ fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS;
   (* FIXME: Lookup in the context every time!!! Fix this !!!*)
  fun splitequation ctxt th acc =
   let
diff -r c46910a6bfce -r 833d154ab189 src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Wed Jan 31 21:05:47 2018 +0100
+++ b/src/HOL/Decision_Procs/langford.ML	Thu Feb 01 13:55:10 2018 +0100
@@ -229,7 +229,7 @@
   let
     fun all x t =
       Thm.apply (Thm.cterm_of ctxt (Logic.all_const (Thm.typ_of_cterm x))) (Thm.lambda x t)
-    val ts = sort (fn (a, b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
+    val ts = sort Thm.fast_term_ord (f p)
     val p' = fold_rev all ts p
   in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
 
diff -r c46910a6bfce -r 833d154ab189 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Jan 31 21:05:47 2018 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Thu Feb 01 13:55:10 2018 +0100
@@ -211,9 +211,9 @@
   FuncUtil.Monomialfunc.fold (fn (m, _) => fn a => max (monomial_multidegree m) a) p 0;
 
 fun poly_variables p =
-  sort FuncUtil.cterm_ord
+  sort Thm.fast_term_ord
     (FuncUtil.Monomialfunc.fold_rev
-      (fn (m, _) => union (is_equal o FuncUtil.cterm_ord) (monomial_variables m)) p []);
+      (fn (m, _) => union (is_equal o Thm.fast_term_ord) (monomial_variables m)) p []);
 
 (* Conversion from HOL term.                                                 *)
 
@@ -750,7 +750,7 @@
 local
   open Conv
   val concl = Thm.dest_arg o Thm.cprop_of
-  fun simple_cterm_ord t u = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS
+  fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS
 in
 (* FIXME: Replace tryfind by get_first !! *)
 fun real_nonlinear_prover proof_method ctxt =
@@ -851,7 +851,7 @@
 
 local
   open Conv
-  fun simple_cterm_ord t u = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS
+  fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS
   val concl = Thm.dest_arg o Thm.cprop_of
   val shuffle1 =
     fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))"
diff -r c46910a6bfce -r 833d154ab189 src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Wed Jan 31 21:05:47 2018 +0100
+++ b/src/HOL/Library/positivstellensatz.ML	Thu Feb 01 13:55:10 2018 +0100
@@ -63,22 +63,17 @@
 structure Intpairfunc = FuncFun(type key = int*int val ord = prod_ord int_ord int_ord);
 structure Symfunc = FuncFun(type key = string val ord = fast_string_ord);
 structure Termfunc = FuncFun(type key = term val ord = Term_Ord.fast_term_ord);
-
-val cterm_ord = Term_Ord.fast_term_ord o apply2 Thm.term_of
-
-structure Ctermfunc = FuncFun(type key = cterm val ord = cterm_ord);
+structure Ctermfunc = FuncFun(type key = cterm val ord = Thm.fast_term_ord);
 
 type monomial = int Ctermfunc.table;
-
-val monomial_ord = list_ord (prod_ord cterm_ord int_ord) o apply2 Ctermfunc.dest
-
+val monomial_ord = list_ord (prod_ord Thm.fast_term_ord int_ord) o apply2 Ctermfunc.dest
 structure Monomialfunc = FuncFun(type key = monomial val ord = monomial_ord)
 
 type poly = Rat.rat Monomialfunc.table;
 
 (* The ordering so we can create canonical HOL polynomials.                  *)
 
-fun dest_monomial mon = sort (cterm_ord o apply2 fst) (Ctermfunc.dest mon);
+fun dest_monomial mon = sort (Thm.fast_term_ord o apply2 fst) (Ctermfunc.dest mon);
 
 fun monomial_order (m1,m2) =
   if Ctermfunc.is_empty m2 then LESS
@@ -91,7 +86,7 @@
       val deg2 = fold (Integer.add o snd) mon2 0
     in if deg1 < deg2 then GREATER
        else if deg1 > deg2 then LESS
-       else list_ord (prod_ord cterm_ord int_ord) (mon1,mon2)
+       else list_ord (prod_ord Thm.fast_term_ord int_ord) (mon1,mon2)
     end;
 
 end
@@ -769,7 +764,7 @@
 
 fun gen_prover_real_arith ctxt prover =
   let
-    fun simple_cterm_ord t u = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS
+    fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS
     val {add, mul, neg, pow = _, sub = _, main} =
         Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
         (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>))
diff -r c46910a6bfce -r 833d154ab189 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Wed Jan 31 21:05:47 2018 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Feb 01 13:55:10 2018 +0100
@@ -803,7 +803,7 @@
  let 
    fun all x t =
     Thm.apply (Thm.cterm_of ctxt (Logic.all_const (Thm.typ_of_cterm x))) (Thm.lambda x t)
-   val ts = sort (fn (a, b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
+   val ts = sort Thm.fast_term_ord (f p)
    val p' = fold_rev all ts p
  in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
 
diff -r c46910a6bfce -r 833d154ab189 src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Wed Jan 31 21:05:47 2018 +0100
+++ b/src/HOL/Tools/groebner.ML	Thu Feb 01 13:55:10 2018 +0100
@@ -646,8 +646,7 @@
   val cjs = conjs tm
   val  rawvars =
     fold_rev (fn eq => fn a => grobvars (Thm.dest_arg1 eq) (grobvars (Thm.dest_arg eq) a)) cjs []
-  val vars = sort (fn (x, y) => Term_Ord.term_ord (Thm.term_of x, Thm.term_of y))
-                  (distinct (op aconvc) rawvars)
+  val vars = sort Thm.term_ord (distinct (op aconvc) rawvars)
  in (vars,map (grobify_equation vars) cjs)
  end;
 
@@ -866,8 +865,7 @@
  let
   val vars = filter (fn v => free_in v eq) evs
   val (qs,p) = isolate_monomials vars eq
-  val rs = ideal (qs @ ps) p
-              (fn (s,t) => Term_Ord.term_ord (Thm.term_of s, Thm.term_of t))
+  val rs = ideal (qs @ ps) p Thm.term_ord
  in (eq, take (length qs) rs ~~ vars)
  end;
  fun subst_in_poly i p = Thm.rhs_of (ring_normalize_conv (vsubst i p));
diff -r c46910a6bfce -r 833d154ab189 src/HOL/Tools/sat.ML
--- a/src/HOL/Tools/sat.ML	Wed Jan 31 21:05:47 2018 +0100
+++ b/src/HOL/Tools/sat.ML	Thu Feb 01 13:55:10 2018 +0100
@@ -303,7 +303,7 @@
     (* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *)
     (* terms sorted in descending order, while only linear for terms      *)
     (* sorted in ascending order                                          *)
-    val sorted_clauses = sort (Term_Ord.fast_term_ord o apply2 Thm.term_of) nontrivial_clauses
+    val sorted_clauses = sort Thm.fast_term_ord nontrivial_clauses
     val _ =
       cond_tracing ctxt (fn () =>
         "Sorted non-trivial clauses:\n" ^
diff -r c46910a6bfce -r 833d154ab189 src/HOL/Tools/semiring_normalizer.ML
--- a/src/HOL/Tools/semiring_normalizer.ML	Wed Jan 31 21:05:47 2018 +0100
+++ b/src/HOL/Tools/semiring_normalizer.ML	Thu Feb 01 13:55:10 2018 +0100
@@ -851,7 +851,7 @@
     addsimps (@{thms eval_nat_numeral} @ @{thms diff_nat_numeral} @ @{thms arith_simps} @ @{thms rel_simps})
     addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}]);
 
-fun simple_cterm_ord t u = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS;
+fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS;
 
 
 (* various normalizing conversions *)
diff -r c46910a6bfce -r 833d154ab189 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Wed Jan 31 21:05:47 2018 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Thu Feb 01 13:55:10 2018 +0100
@@ -415,7 +415,7 @@
 local
 
 fun equal_cterms ts us =
-  is_equal (list_ord (Term_Ord.fast_term_ord o apply2 Thm.term_of) (ts, us));
+  is_equal (list_ord Thm.fast_term_ord (ts, us));
 
 fun prep_rule n th =
   let
diff -r c46910a6bfce -r 833d154ab189 src/Pure/more_thm.ML
--- 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;