src/HOL/Multivariate_Analysis/normarith.ML

--- a/src/HOL/Multivariate_Analysis/normarith.ML	Sat Jul 18 20:53:05 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML	Sat Jul 18 20:54:56 2015 +0200
@@ -401,6 +401,6 @@
  fun norm_arith_tac ctxt =
    clarify_tac (put_claset HOL_cs ctxt) THEN'
    Object_Logic.full_atomize_tac ctxt THEN'
-   CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i);
+   CSUBGOAL ( fn (p,i) => resolve_tac ctxt [norm_arith ctxt (Thm.dest_arg p )] i);
 
 end;