src/HOL/Multivariate_Analysis/normarith.ML
changeset 42793 88bee9f6eec7
parent 42361 23f352990944
child 43333 2bdec7f430d3
     1.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Fri May 13 16:03:03 2011 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Fri May 13 22:55:00 2011 +0200
     1.3 @@ -384,7 +384,7 @@
     1.4   end
     1.5  
     1.6   fun norm_arith_tac ctxt =
     1.7 -   clarify_tac HOL_cs THEN'
     1.8 +   clarify_tac (put_claset HOL_cs ctxt) THEN'
     1.9     Object_Logic.full_atomize_tac THEN'
    1.10     CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i);
    1.11