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