src/HOL/Multivariate_Analysis/normarith.ML

--- a/src/HOL/Multivariate_Analysis/normarith.ML	Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML	Fri May 13 22:55:00 2011 +0200
@@ -384,7 +384,7 @@
  end
 
  fun norm_arith_tac ctxt =
-   clarify_tac HOL_cs THEN'
+   clarify_tac (put_claset HOL_cs ctxt) THEN'
    Object_Logic.full_atomize_tac THEN'
    CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i);