src/HOL/Library/positivstellensatz.ML

--- a/src/HOL/Library/positivstellensatz.ML	Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Library/positivstellensatz.ML	Sat Feb 27 23:13:01 2010 +0100
@@ -61,9 +61,9 @@
 structure Ratfunc = FuncFun(type key = Rat.rat val ord = Rat.ord);
 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 = TermOrd.fast_term_ord);
+structure Termfunc = FuncFun(type key = term val ord = Term_Ord.fast_term_ord);
 
-val cterm_ord = TermOrd.fast_term_ord o pairself term_of
+val cterm_ord = Term_Ord.fast_term_ord o pairself term_of
 
 structure Ctermfunc = FuncFun(type key = cterm val ord = cterm_ord);
 
@@ -745,7 +745,7 @@
 
 fun gen_prover_real_arith ctxt prover = 
  let
-  fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS
+  fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS
   val {add,mul,neg,pow,sub,main} = 
      Normalizer.semiring_normalizers_ord_wrapper ctxt
       (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))