src/HOL/Tools/Meson/meson.ML
changeset 60696 8304fb4fb823
parent 60642 48dd1cefb4ae
child 60781 2da59cdf531c
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Wed Jul 08 19:28:43 2015 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Wed Jul 08 21:33:00 2015 +0200
     1.3 @@ -709,7 +709,7 @@
     1.4              resolve_tac ctxt @{thms ccontr} 1,
     1.5              preskolem_tac,
     1.6              Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
     1.7 -                      EVERY1 [skolemize_prems_tac ctxt negs,
     1.8 +                      EVERY1 [skolemize_prems_tac ctxt' negs,
     1.9                                Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
    1.10    handle THM _ => no_tac st;    (*probably from make_meta_clause, not first-order*)
    1.11