src/HOL/Tools/Meson/meson.ML
changeset 55990 41c6b99c5fb7
parent 54742 7a86358a3c0b
child 56245 84fc7dfa3cd4
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Fri Mar 07 22:19:52 2014 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Fri Mar 07 22:30:58 2014 +0100
     1.3 @@ -707,7 +707,7 @@
     1.4  fun MESON preskolem_tac mkcl cltac ctxt i st =
     1.5    SELECT_GOAL
     1.6      (EVERY [Object_Logic.atomize_prems_tac ctxt 1,
     1.7 -            rtac ccontr 1,
     1.8 +            rtac @{thm ccontr} 1,
     1.9              preskolem_tac,
    1.10              Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
    1.11                        EVERY1 [skolemize_prems_tac ctxt negs,