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