src/HOL/Library/Sum_of_Squares/sum_of_squares.ML

--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Fri Dec 13 23:53:02 2013 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sat Dec 14 17:28:05 2013 +0100
@@ -938,7 +938,7 @@
 fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
 
 fun sos_tac print_cert prover ctxt =
-  Object_Logic.full_atomize_tac THEN'
+  Object_Logic.full_atomize_tac ctxt THEN'
   elim_denom_tac ctxt THEN'
   core_sos_tac print_cert prover ctxt;