src/HOL/Tools/Meson/meson.ML

--- a/src/HOL/Tools/Meson/meson.ML	Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/Meson/meson.ML	Fri Mar 07 22:30:58 2014 +0100
@@ -707,7 +707,7 @@
 fun MESON preskolem_tac mkcl cltac ctxt i st =
   SELECT_GOAL
     (EVERY [Object_Logic.atomize_prems_tac ctxt 1,
-            rtac ccontr 1,
+            rtac @{thm ccontr} 1,
             preskolem_tac,
             Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
                       EVERY1 [skolemize_prems_tac ctxt negs,