--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Wed May 05 16:53:21 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Thu May 06 16:32:20 2010 +0200
@@ -1195,7 +1195,7 @@
fun real_nonlinear_prover proof_method ctxt =
let
val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt
- (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
+ (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
simple_cterm_ord
val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv,
real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main)
@@ -1310,7 +1310,7 @@
fun real_nonlinear_subst_prover prover ctxt =
let
val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt
- (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
+ (the (Normalizer.match ctxt @{cterm "(0::real) + 1"}))
simple_cterm_ord
val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv,