author | paulson |
Tue, 03 Jul 2007 21:56:25 +0200 | |
changeset 23552 | 6403d06abe25 |
parent 23551 | 84f0996a530b |
child 23553 | af8ae54238f5 |
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