src/HOL/Library/positivstellensatz.ML
changeset 35408 b48ab741683b
parent 35028 108662d50512
child 36700 9b85b9d74b83
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Sat Feb 27 22:52:25 2010 +0100
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Sat Feb 27 23:13:01 2010 +0100
     1.3 @@ -61,9 +61,9 @@
     1.4  structure Ratfunc = FuncFun(type key = Rat.rat val ord = Rat.ord);
     1.5  structure Intpairfunc = FuncFun(type key = int*int val ord = prod_ord int_ord int_ord);
     1.6  structure Symfunc = FuncFun(type key = string val ord = fast_string_ord);
     1.7 -structure Termfunc = FuncFun(type key = term val ord = TermOrd.fast_term_ord);
     1.8 +structure Termfunc = FuncFun(type key = term val ord = Term_Ord.fast_term_ord);
     1.9  
    1.10 -val cterm_ord = TermOrd.fast_term_ord o pairself term_of
    1.11 +val cterm_ord = Term_Ord.fast_term_ord o pairself term_of
    1.12  
    1.13  structure Ctermfunc = FuncFun(type key = cterm val ord = cterm_ord);
    1.14  
    1.15 @@ -745,7 +745,7 @@
    1.16  
    1.17  fun gen_prover_real_arith ctxt prover = 
    1.18   let
    1.19 -  fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS
    1.20 +  fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS
    1.21    val {add,mul,neg,pow,sub,main} = 
    1.22       Normalizer.semiring_normalizers_ord_wrapper ctxt
    1.23        (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))