1.1 --- a/src/HOL/Tools/meson.ML	Thu Jul 05 19:59:01 2007 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Thu Jul 05 20:01:26 2007 +0200
     1.3 @@ -556,7 +556,7 @@
     1.4    Function mkcl converts theorems to clauses.*)
     1.5  fun MESON mkcl cltac i st = 
     1.6    SELECT_GOAL
     1.7 -    (EVERY [ObjectLogic.atomize_tac 1,
     1.8 +    (EVERY [ObjectLogic.atomize_prems_tac 1,
     1.9              rtac ccontr 1,
    1.10  	    METAHYPS (fn negs =>
    1.11  		      EVERY1 [skolemize_prems_tac negs,