changeset 35625 | 9c818cab0dd0 |
parent 35410 | 1ea89d2a1bd4 |
child 35845 | e5980f0ad025 |
child 35869 | cac366550624 |
--- a/src/HOL/Tools/meson.ML Sun Mar 07 11:57:16 2010 +0100 +++ b/src/HOL/Tools/meson.ML Sun Mar 07 12:19:47 2010 +0100 @@ -587,7 +587,7 @@ Function mkcl converts theorems to clauses.*) fun MESON mkcl cltac ctxt i st = SELECT_GOAL - (EVERY [ObjectLogic.atomize_prems_tac 1, + (EVERY [Object_Logic.atomize_prems_tac 1, rtac ccontr 1, Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} => EVERY1 [skolemize_prems_tac ctxt negs,