Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reduced warnings;
authorwenzelm
Sun, 10 Aug 2014 20:45:48 +0200
changeset 57889 049e13f616d4
parent 57888 9c193dcc8ec8
child 57890 1e13f63fb452
reduced warnings;
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML file | annotate | diff | comparison | revisions 
--- 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'
isabelle