local simpset_of;

--- 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}