src/HOL/Library/Sum_of_Squares/sum_of_squares.ML

 
 fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
 
 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'
   end;