src/HOL/Tools/meson.ML
changeset 32283 3bebc195c124
parent 32262 73cd8f74cf2a
child 32740 9dd0a2f83429
     1.1 --- a/src/HOL/Tools/meson.ML	Thu Jul 30 11:23:57 2009 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Thu Jul 30 12:20:43 2009 +0200
     1.3 @@ -586,9 +586,9 @@
     1.4    SELECT_GOAL
     1.5      (EVERY [ObjectLogic.atomize_prems_tac 1,
     1.6              rtac ccontr 1,
     1.7 -            FOCUS (fn {context = ctxt', prems = negs, ...} =>
     1.8 +            Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
     1.9                        EVERY1 [skolemize_prems_tac ctxt negs,
    1.10 -                              FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
    1.11 +                              Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
    1.12    handle THM _ => no_tac st;    (*probably from make_meta_clause, not first-order*)
    1.13  
    1.14  (** Best-first search versions **)