--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Sun Aug 10 19:53:30 2014 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Sun Aug 10 20:45:48 2014 +0200
@@ -1048,7 +1048,7 @@
fun sos_tac print_cert prover ctxt =
(* The SOS prover breaks if mult_nonneg_nonneg is in the simpset *)
- let val ctxt' = ctxt delsimps [@{thm mult_nonneg_nonneg}]
+ let val ctxt' = Context_Position.set_visible false ctxt delsimps @{thms mult_nonneg_nonneg}
in Object_Logic.full_atomize_tac ctxt' THEN'
elim_denom_tac ctxt' THEN'
core_sos_tac print_cert prover ctxt'