# HG changeset patch
# User wenzelm
# Date 1248367449 -7200
# Node ID 4ed2865f3a56257790060a613b89ae1e34d94947
# Parent  ef59550a55d32607bf70c95829a72cf898947c5b
local simpset_of;

diff -r ef59550a55d3 -r 4ed2865f3a56 src/HOL/Library/sum_of_squares.ML
--- a/src/HOL/Library/sum_of_squares.ML	Thu Jul 23 18:44:09 2009 +0200
+++ b/src/HOL/Library/sum_of_squares.ML	Thu Jul 23 18:44:09 2009 +0200
@@ -1686,7 +1686,7 @@
    NONE => no_tac
  | SOME (d,ord) => 
      let 
-      val ss = simpset_of (ProofContext.theory_of ctxt) addsimps @{thms field_simps} 
+      val ss = simpset_of ctxt addsimps @{thms field_simps} 
                addsimps [@{thm nonzero_power_divide}, @{thm power_divide}]
       val th = instantiate' [] [SOME d, SOME (Thm.dest_arg P)] 
          (if ord then @{lemma "(d=0 --> P) & (d>0 --> P) & (d<(0::real) --> P) ==> P" by auto}