1.1 --- a/src/HOL/Tools/meson.ML	Tue Jul 03 20:26:08 2007 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Tue Jul 03 21:56:25 2007 +0200
     1.3 @@ -556,7 +556,8 @@
     1.4    Function mkcl converts theorems to clauses.*)
     1.5  fun MESON mkcl cltac i st = 
     1.6    SELECT_GOAL
     1.7 -    (EVERY [rtac ccontr 1,
     1.8 +    (EVERY [ObjectLogic.atomize_tac 1,
     1.9 +            rtac ccontr 1,
    1.10  	    METAHYPS (fn negs =>
    1.11  		      EVERY1 [skolemize_prems_tac negs,
    1.12  			      METAHYPS (cltac o mkcl)]) 1]) i st