to handle non-atomic assumptions
authorpaulson
Tue Jul 03 21:56:25 2007 +0200 (2007-07-03)
changeset 235526403d06abe25
parent 23551 84f0996a530b
child 23553 af8ae54238f5
to handle non-atomic assumptions
src/HOL/Tools/meson.ML
     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