src/HOL/Multivariate_Analysis/normarith.ML

--- a/src/HOL/Multivariate_Analysis/normarith.ML	Fri Dec 13 23:53:02 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/normarith.ML	Sat Dec 14 17:28:05 2013 +0100
@@ -399,7 +399,7 @@
 
  fun norm_arith_tac ctxt =
    clarify_tac (put_claset HOL_cs ctxt) THEN'
-   Object_Logic.full_atomize_tac THEN'
+   Object_Logic.full_atomize_tac ctxt THEN'
    CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i);
 
 end;