# HG changeset patch
# User paulson
# Date 1183492585 -7200
# Node ID 6403d06abe256b7b7aa40822383f213eb75cdef9
# Parent  84f0996a530bfc69ddc83522a1bf63acd1388945
to handle non-atomic assumptions

diff -r 84f0996a530b -r 6403d06abe25 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Tue Jul 03 20:26:08 2007 +0200
+++ b/src/HOL/Tools/meson.ML	Tue Jul 03 21:56:25 2007 +0200
@@ -556,7 +556,8 @@
   Function mkcl converts theorems to clauses.*)
 fun MESON mkcl cltac i st = 
   SELECT_GOAL
-    (EVERY [rtac ccontr 1,
+    (EVERY [ObjectLogic.atomize_tac 1,
+            rtac ccontr 1,
 	    METAHYPS (fn negs =>
 		      EVERY1 [skolemize_prems_tac negs,
 			      METAHYPS (cltac o mkcl)]) 1]) i st