src/HOL/Tools/meson.ML

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