diff -r 9c193dcc8ec8 -r 049e13f616d4 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- 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'