src/HOL/Multivariate_Analysis/normarith.ML

   in Thm.equal_elim (Drule.arg_cong_rule @{cterm Trueprop} (Thm.symmetric th))
                 (pure ctxt' (Thm.rhs_of th))
  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);
 
 end;