src/HOL/Library/positivstellensatz.ML
changeset 67559 833d154ab189
parent 67399 eab6ce8368fa
child 67560 0fa87bd86566
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Jan 31 21:05:47 2018 +0100
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu Feb 01 13:55:10 2018 +0100
     1.3 @@ -63,22 +63,17 @@
     1.4  structure Intpairfunc = FuncFun(type key = int*int val ord = prod_ord int_ord int_ord);
     1.5  structure Symfunc = FuncFun(type key = string val ord = fast_string_ord);
     1.6  structure Termfunc = FuncFun(type key = term val ord = Term_Ord.fast_term_ord);
     1.7 -
     1.8 -val cterm_ord = Term_Ord.fast_term_ord o apply2 Thm.term_of
     1.9 -
    1.10 -structure Ctermfunc = FuncFun(type key = cterm val ord = cterm_ord);
    1.11 +structure Ctermfunc = FuncFun(type key = cterm val ord = Thm.fast_term_ord);
    1.12  
    1.13  type monomial = int Ctermfunc.table;
    1.14 -
    1.15 -val monomial_ord = list_ord (prod_ord cterm_ord int_ord) o apply2 Ctermfunc.dest
    1.16 -
    1.17 +val monomial_ord = list_ord (prod_ord Thm.fast_term_ord int_ord) o apply2 Ctermfunc.dest
    1.18  structure Monomialfunc = FuncFun(type key = monomial val ord = monomial_ord)
    1.19  
    1.20  type poly = Rat.rat Monomialfunc.table;
    1.21  
    1.22  (* The ordering so we can create canonical HOL polynomials.                  *)
    1.23  
    1.24 -fun dest_monomial mon = sort (cterm_ord o apply2 fst) (Ctermfunc.dest mon);
    1.25 +fun dest_monomial mon = sort (Thm.fast_term_ord o apply2 fst) (Ctermfunc.dest mon);
    1.26  
    1.27  fun monomial_order (m1,m2) =
    1.28    if Ctermfunc.is_empty m2 then LESS
    1.29 @@ -91,7 +86,7 @@
    1.30        val deg2 = fold (Integer.add o snd) mon2 0
    1.31      in if deg1 < deg2 then GREATER
    1.32         else if deg1 > deg2 then LESS
    1.33 -       else list_ord (prod_ord cterm_ord int_ord) (mon1,mon2)
    1.34 +       else list_ord (prod_ord Thm.fast_term_ord int_ord) (mon1,mon2)
    1.35      end;
    1.36  
    1.37  end
    1.38 @@ -769,7 +764,7 @@
    1.39  
    1.40  fun gen_prover_real_arith ctxt prover =
    1.41    let
    1.42 -    fun simple_cterm_ord t u = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS
    1.43 +    fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS
    1.44      val {add, mul, neg, pow = _, sub = _, main} =
    1.45          Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
    1.46          (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>))