merged
authorwenzelm
Wed Jul 29 19:36:22 2009 +0200 (2009-07-29)
changeset 32275b10cbf4d3f55
parent 32274 e7f275d203bc
parent 32262 73cd8f74cf2a
child 32276 756afe4a909a
child 32277 ff1e59a15146
merged
     1.1 --- a/src/FOL/FOL.thy	Wed Jul 29 16:43:02 2009 +0200
     1.2 +++ b/src/FOL/FOL.thy	Wed Jul 29 19:36:22 2009 +0200
     1.3 @@ -168,7 +168,7 @@
     1.4  
     1.5  use "cladata.ML"
     1.6  setup Cla.setup
     1.7 -setup cla_setup
     1.8 +ML {* Context.>> (Cla.map_cs (K FOL_cs)) *}
     1.9  
    1.10  ML {*
    1.11    structure Blast = Blast
     2.1 --- a/src/FOL/cladata.ML	Wed Jul 29 16:43:02 2009 +0200
     2.2 +++ b/src/FOL/cladata.ML	Wed Jul 29 19:36:22 2009 +0200
     2.3 @@ -32,4 +32,3 @@
     2.4  val FOL_cs = prop_cs addSIs [@{thm allI}, @{thm ex_ex1I}] addIs [@{thm exI}]
     2.5                       addSEs [@{thm exE}, @{thm alt_ex1E}] addEs [@{thm allE}];
     2.6  
     2.7 -val cla_setup = Cla.map_claset (K FOL_cs);
     3.1 --- a/src/HOL/Prolog/prolog.ML	Wed Jul 29 16:43:02 2009 +0200
     3.2 +++ b/src/HOL/Prolog/prolog.ML	Wed Jul 29 19:36:22 2009 +0200
     3.3 @@ -67,8 +67,8 @@
     3.4          imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
     3.5          imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
     3.6  
     3.7 -(*val hyp_resolve_tac = METAHYPS (fn prems =>
     3.8 -                                  resolve_tac (List.concat (map atomizeD prems)) 1);
     3.9 +(*val hyp_resolve_tac = FOCUS (fn {prems, ...} =>
    3.10 +                                  resolve_tac (maps atomizeD prems) 1);
    3.11    -- is nice, but cannot instantiate unknowns in the assumptions *)
    3.12  fun hyp_resolve_tac i st = let
    3.13          fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
     4.1 --- a/src/HOL/Tools/meson.ML	Wed Jul 29 16:43:02 2009 +0200
     4.2 +++ b/src/HOL/Tools/meson.ML	Wed Jul 29 19:36:22 2009 +0200
     4.3 @@ -14,30 +14,29 @@
     4.4    val too_many_clauses: Proof.context option -> term -> bool
     4.5    val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
     4.6    val finish_cnf: thm list -> thm list
     4.7 -  val make_nnf: thm -> thm
     4.8 -  val skolemize: thm -> thm
     4.9 +  val make_nnf: Proof.context -> thm -> thm
    4.10 +  val skolemize: Proof.context -> thm -> thm
    4.11    val is_fol_term: theory -> term -> bool
    4.12    val make_clauses: thm list -> thm list
    4.13    val make_horns: thm list -> thm list
    4.14    val best_prolog_tac: (thm -> int) -> thm list -> tactic
    4.15    val depth_prolog_tac: thm list -> tactic
    4.16    val gocls: thm list -> thm list
    4.17 -  val skolemize_prems_tac: thm list -> int -> tactic
    4.18 -  val MESON: (thm list -> thm list) -> (thm list -> tactic) -> int -> tactic
    4.19 -  val best_meson_tac: (thm -> int) -> int -> tactic
    4.20 -  val safe_best_meson_tac: claset -> int -> tactic
    4.21 -  val depth_meson_tac: int -> tactic
    4.22 +  val skolemize_prems_tac: Proof.context -> thm list -> int -> tactic
    4.23 +  val MESON: (thm list -> thm list) -> (thm list -> tactic) -> Proof.context -> int -> tactic
    4.24 +  val best_meson_tac: (thm -> int) -> Proof.context -> int -> tactic
    4.25 +  val safe_best_meson_tac: Proof.context -> int -> tactic
    4.26 +  val depth_meson_tac: Proof.context -> int -> tactic
    4.27    val prolog_step_tac': thm list -> int -> tactic
    4.28    val iter_deepen_prolog_tac: thm list -> tactic
    4.29 -  val iter_deepen_meson_tac: thm list -> int -> tactic
    4.30 +  val iter_deepen_meson_tac: Proof.context -> thm list -> int -> tactic
    4.31    val make_meta_clause: thm -> thm
    4.32    val make_meta_clauses: thm list -> thm list
    4.33 -  val meson_claset_tac: thm list -> claset -> int -> tactic
    4.34 -  val meson_tac: claset -> int -> tactic
    4.35 +  val meson_tac: Proof.context -> thm list -> int -> tactic
    4.36    val negate_head: thm -> thm
    4.37    val select_literal: int -> thm -> thm
    4.38 -  val skolemize_tac: int -> tactic
    4.39 -  val setup: Context.theory -> Context.theory
    4.40 +  val skolemize_tac: Proof.context -> int -> tactic
    4.41 +  val setup: theory -> theory
    4.42  end
    4.43  
    4.44  structure Meson: MESON =
    4.45 @@ -89,13 +88,16 @@
    4.46  
    4.47  (*FIXME: currently does not "rename variables apart"*)
    4.48  fun first_order_resolve thA thB =
    4.49 -  let val thy = theory_of_thm thA
    4.50 -      val tmA = concl_of thA
    4.51 -      val Const("==>",_) $ tmB $ _ = prop_of thB
    4.52 -      val (tyenv, tenv) = Pattern.first_order_match thy (tmB, tmA) (Vartab.empty, Vartab.empty)
    4.53 -      val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
    4.54 -  in  thA RS (cterm_instantiate ct_pairs thB)  end
    4.55 -  handle _ => raise THM ("first_order_resolve", 0, [thA,thB]);  (* FIXME avoid handle _ *)
    4.56 +  (case
    4.57 +    try (fn () =>
    4.58 +      let val thy = theory_of_thm thA
    4.59 +          val tmA = concl_of thA
    4.60 +          val Const("==>",_) $ tmB $ _ = prop_of thB
    4.61 +          val (tyenv, tenv) = Pattern.first_order_match thy (tmB, tmA) (Vartab.empty, Vartab.empty)
    4.62 +          val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
    4.63 +      in  thA RS (cterm_instantiate ct_pairs thB)  end) () of
    4.64 +    SOME th => th
    4.65 +  | NONE => raise THM ("first_order_resolve", 0, [thA, thB]));
    4.66  
    4.67  fun flexflex_first_order th =
    4.68    case (tpairs_of th) of
    4.69 @@ -124,13 +126,13 @@
    4.70    e.g. from conj_forward, should have the form
    4.71      "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
    4.72    and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
    4.73 -fun forward_res nf st =
    4.74 +fun forward_res ctxt nf st =
    4.75    let fun forward_tacf [prem] = rtac (nf prem) 1
    4.76          | forward_tacf prems =
    4.77              error (cat_lines
    4.78                ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
    4.79 -                Display.string_of_thm_without_context st ::
    4.80 -                "Premises:" :: map Display.string_of_thm_without_context prems))
    4.81 +                Display.string_of_thm ctxt st ::
    4.82 +                "Premises:" :: map (Display.string_of_thm ctxt) prems))
    4.83    in
    4.84      case Seq.pull (ALLGOALS (OldGoals.METAHYPS forward_tacf) st)
    4.85      of SOME(th,_) => th
    4.86 @@ -223,7 +225,7 @@
    4.87  (*** Removal of duplicate literals ***)
    4.88  
    4.89  (*Forward proof, passing extra assumptions as theorems to the tactic*)
    4.90 -fun forward_res2 nf hyps st =
    4.91 +fun forward_res2 ctxt nf hyps st =
    4.92    case Seq.pull
    4.93          (REPEAT
    4.94           (OldGoals.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
    4.95 @@ -233,16 +235,16 @@
    4.96  
    4.97  (*Remove duplicates in P|Q by assuming ~P in Q
    4.98    rls (initially []) accumulates assumptions of the form P==>False*)
    4.99 -fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
   4.100 +fun nodups_aux ctxt rls th = nodups_aux ctxt rls (th RS disj_assoc)
   4.101      handle THM _ => tryres(th,rls)
   4.102 -    handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
   4.103 +    handle THM _ => tryres(forward_res2 ctxt (nodups_aux ctxt) rls (th RS disj_forward2),
   4.104                             [disj_FalseD1, disj_FalseD2, asm_rl])
   4.105      handle THM _ => th;
   4.106  
   4.107  (*Remove duplicate literals, if there are any*)
   4.108 -fun nodups th =
   4.109 +fun nodups ctxt th =
   4.110    if has_duplicates (op =) (literals (prop_of th))
   4.111 -    then nodups_aux [] th
   4.112 +    then nodups_aux ctxt [] th
   4.113      else th;
   4.114  
   4.115  
   4.116 @@ -321,7 +323,7 @@
   4.117        fun cnf_aux (th,ths) =
   4.118          if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
   4.119          else if not (has_conns ["All","Ex","op &"] (prop_of th))
   4.120 -        then nodups th :: ths (*no work to do, terminate*)
   4.121 +        then nodups ctxt th :: ths (*no work to do, terminate*)
   4.122          else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
   4.123              Const ("op &", _) => (*conjunction*)
   4.124                  cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
   4.125 @@ -335,10 +337,10 @@
   4.126                (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
   4.127                  all combinations of converting P, Q to CNF.*)
   4.128                let val tac =
   4.129 -                  (OldGoals.METAHYPS (resop cnf_nil) 1) THEN
   4.130 +                  OldGoals.METAHYPS (resop cnf_nil) 1 THEN
   4.131                     (fn st' => st' |> OldGoals.METAHYPS (resop cnf_nil) 1)
   4.132                in  Seq.list_of (tac (th RS disj_forward)) @ ths  end
   4.133 -          | _ => nodups th :: ths  (*no work to do*)
   4.134 +          | _ => nodups ctxt th :: ths  (*no work to do*)
   4.135        and cnf_nil th = cnf_aux (th,[])
   4.136        val cls = 
   4.137  	    if too_many_clauses (SOME ctxt) (concl_of th)
   4.138 @@ -499,11 +501,11 @@
   4.139    | ok4nnf (Const ("Trueprop",_) $ t) = rigid t
   4.140    | ok4nnf _ = false;
   4.141  
   4.142 -fun make_nnf1 th =
   4.143 +fun make_nnf1 ctxt th =
   4.144    if ok4nnf (concl_of th)
   4.145 -  then make_nnf1 (tryres(th, nnf_rls))
   4.146 +  then make_nnf1 ctxt (tryres(th, nnf_rls))
   4.147      handle THM ("tryres", _, _) =>
   4.148 -        forward_res make_nnf1
   4.149 +        forward_res ctxt (make_nnf1 ctxt)
   4.150             (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
   4.151      handle THM ("tryres", _, _) => th
   4.152    else th;
   4.153 @@ -521,32 +523,32 @@
   4.154    HOL_basic_ss addsimps nnf_extra_simps
   4.155      addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
   4.156  
   4.157 -fun make_nnf th = case prems_of th of
   4.158 +fun make_nnf ctxt th = case prems_of th of
   4.159      [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
   4.160               |> simplify nnf_ss
   4.161 -             |> make_nnf1
   4.162 +             |> make_nnf1 ctxt
   4.163    | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
   4.164  
   4.165  (*Pull existential quantifiers to front. This accomplishes Skolemization for
   4.166    clauses that arise from a subgoal.*)
   4.167 -fun skolemize1 th =
   4.168 +fun skolemize1 ctxt th =
   4.169    if not (has_conns ["Ex"] (prop_of th)) then th
   4.170 -  else (skolemize1 (tryres(th, [choice, conj_exD1, conj_exD2,
   4.171 +  else (skolemize1 ctxt (tryres(th, [choice, conj_exD1, conj_exD2,
   4.172                                disj_exD, disj_exD1, disj_exD2])))
   4.173      handle THM ("tryres", _, _) =>
   4.174 -        skolemize1 (forward_res skolemize1
   4.175 +        skolemize1 ctxt (forward_res ctxt (skolemize1 ctxt)
   4.176                     (tryres (th, [conj_forward, disj_forward, all_forward])))
   4.177      handle THM ("tryres", _, _) => 
   4.178 -        forward_res skolemize1 (rename_bvs_RS th ex_forward);
   4.179 +        forward_res ctxt (skolemize1 ctxt) (rename_bvs_RS th ex_forward);
   4.180  
   4.181 -fun skolemize th = skolemize1 (make_nnf th);
   4.182 +fun skolemize ctxt th = skolemize1 ctxt (make_nnf ctxt th);
   4.183  
   4.184 -fun skolemize_nnf_list [] = []
   4.185 -  | skolemize_nnf_list (th::ths) = 
   4.186 -      skolemize th :: skolemize_nnf_list ths
   4.187 +fun skolemize_nnf_list _ [] = []
   4.188 +  | skolemize_nnf_list ctxt (th::ths) =
   4.189 +      skolemize ctxt th :: skolemize_nnf_list ctxt ths
   4.190        handle THM _ => (*RS can fail if Unify.search_bound is too small*)
   4.191 -       (warning ("Failed to Skolemize " ^ Display.string_of_thm_without_context th);
   4.192 -        skolemize_nnf_list ths);
   4.193 +       (warning ("Failed to Skolemize " ^ Display.string_of_thm ctxt th);
   4.194 +        skolemize_nnf_list ctxt ths);
   4.195  
   4.196  fun add_clauses (th,cls) =
   4.197    let val ctxt0 = Variable.thm_context th
   4.198 @@ -574,19 +576,19 @@
   4.199  (*Return all negative clauses, as possible goal clauses*)
   4.200  fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
   4.201  
   4.202 -fun skolemize_prems_tac prems =
   4.203 -    cut_facts_tac (skolemize_nnf_list prems) THEN'
   4.204 +fun skolemize_prems_tac ctxt prems =
   4.205 +    cut_facts_tac (skolemize_nnf_list ctxt prems) THEN'
   4.206      REPEAT o (etac exE);
   4.207  
   4.208  (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions.
   4.209    Function mkcl converts theorems to clauses.*)
   4.210 -fun MESON mkcl cltac i st =
   4.211 +fun MESON mkcl cltac ctxt i st =
   4.212    SELECT_GOAL
   4.213      (EVERY [ObjectLogic.atomize_prems_tac 1,
   4.214              rtac ccontr 1,
   4.215 -            OldGoals.METAHYPS (fn negs =>
   4.216 -                      EVERY1 [skolemize_prems_tac negs,
   4.217 -                              OldGoals.METAHYPS (cltac o mkcl)]) 1]) i st
   4.218 +            FOCUS (fn {context = ctxt', prems = negs, ...} =>
   4.219 +                      EVERY1 [skolemize_prems_tac ctxt negs,
   4.220 +                              FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
   4.221    handle THM _ => no_tac st;    (*probably from make_meta_clause, not first-order*)
   4.222  
   4.223  (** Best-first search versions **)
   4.224 @@ -600,9 +602,9 @@
   4.225                           (prolog_step_tac (make_horns cls) 1));
   4.226  
   4.227  (*First, breaks the goal into independent units*)
   4.228 -fun safe_best_meson_tac cs =
   4.229 -     SELECT_GOAL (TRY (safe_tac cs) THEN
   4.230 -                  TRYALL (best_meson_tac size_of_subgoals));
   4.231 +fun safe_best_meson_tac ctxt =
   4.232 +     SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN
   4.233 +                  TRYALL (best_meson_tac size_of_subgoals ctxt));
   4.234  
   4.235  (** Depth-first search version **)
   4.236  
   4.237 @@ -627,7 +629,7 @@
   4.238  fun iter_deepen_prolog_tac horns =
   4.239      ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
   4.240  
   4.241 -fun iter_deepen_meson_tac ths = MESON make_clauses
   4.242 +fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON make_clauses
   4.243    (fn cls =>
   4.244      (case (gocls (cls @ ths)) of
   4.245        [] => no_tac  (*no goal clauses*)
   4.246 @@ -636,14 +638,12 @@
   4.247            val horns = make_horns (cls @ ths)
   4.248            val _ = Output.debug (fn () =>
   4.249              cat_lines ("meson method called:" ::
   4.250 -              map Display.string_of_thm_without_context (cls @ ths) @
   4.251 -              ["clauses:"] @ map Display.string_of_thm_without_context horns))
   4.252 +              map (Display.string_of_thm ctxt) (cls @ ths) @
   4.253 +              ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
   4.254          in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) end));
   4.255  
   4.256 -fun meson_claset_tac ths cs =
   4.257 -  SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
   4.258 -
   4.259 -val meson_tac = meson_claset_tac [];
   4.260 +fun meson_tac ctxt ths =
   4.261 +  SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths));
   4.262  
   4.263  
   4.264  (**** Code to support ordinary resolution, rather than Model Elimination ****)
   4.265 @@ -695,14 +695,14 @@
   4.266    leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
   4.267    might generate many subgoals.*)
   4.268  
   4.269 -fun skolemize_tac i st =
   4.270 -  let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
   4.271 +fun skolemize_tac ctxt = SUBGOAL (fn (goal, i) =>
   4.272 +  let val ts = Logic.strip_assums_hyp goal
   4.273    in
   4.274 -     EVERY' [OldGoals.METAHYPS
   4.275 -            (fn hyps => (cut_facts_tac (skolemize_nnf_list hyps) 1
   4.276 -                         THEN REPEAT (etac exE 1))),
   4.277 -            REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st
   4.278 -  end
   4.279 -  handle Subscript => Seq.empty;
   4.280 +    EVERY'
   4.281 +     [OldGoals.METAHYPS (fn hyps =>
   4.282 +        (cut_facts_tac (skolemize_nnf_list ctxt hyps) 1
   4.283 +          THEN REPEAT (etac exE 1))),
   4.284 +      REPEAT_DETERM_N (length ts) o (etac thin_rl)] i
   4.285 +  end);
   4.286  
   4.287  end;
     5.1 --- a/src/HOL/Tools/metis_tools.ML	Wed Jul 29 16:43:02 2009 +0200
     5.2 +++ b/src/HOL/Tools/metis_tools.ML	Wed Jul 29 19:36:22 2009 +0200
     5.3 @@ -628,7 +628,8 @@
     5.4         if exists_type ResAxioms.type_has_empty_sort (prop_of st0)  
     5.5         then (warning "Proof state contains the empty sort"; Seq.empty)
     5.6         else 
     5.7 -	 (Meson.MESON ResAxioms.neg_clausify (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) i
     5.8 +	 (Meson.MESON ResAxioms.neg_clausify
     5.9 +	   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
    5.10  	  THEN ResAxioms.expand_defs_tac st0) st0
    5.11      end
    5.12      handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
     6.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Jul 29 16:43:02 2009 +0200
     6.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Jul 29 19:36:22 2009 +0200
     6.3 @@ -270,8 +270,10 @@
     6.4  (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
     6.5  fun to_nnf th ctxt0 =
     6.6    let val th1 = th |> transform_elim |> zero_var_indexes
     6.7 -      val ((_,[th2]),ctxt) = Variable.import true [th1] ctxt0
     6.8 -      val th3 = th2 |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1
     6.9 +      val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
    6.10 +      val th3 = th2
    6.11 +        |> Conv.fconv_rule ObjectLogic.atomize
    6.12 +        |> Meson.make_nnf ctxt |> strip_lambdas ~1
    6.13    in  (th3, ctxt)  end;
    6.14  
    6.15  (*Generate Skolem functions for a theorem supplied in nnf*)
    6.16 @@ -483,33 +485,35 @@
    6.17    in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
    6.18  
    6.19  
    6.20 -fun meson_general_tac ths i st0 =
    6.21 +fun meson_general_tac ctxt ths i st0 =
    6.22    let
    6.23 -    val thy = Thm.theory_of_thm st0
    6.24 -  in  (Meson.meson_claset_tac (maps (cnf_axiom thy) ths) HOL_cs i THEN expand_defs_tac st0) st0 end;
    6.25 +    val thy = ProofContext.theory_of ctxt
    6.26 +    val ctxt0 = Classical.put_claset HOL_cs ctxt
    6.27 +  in (Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) i THEN expand_defs_tac st0) st0 end;
    6.28  
    6.29  val meson_method_setup =
    6.30 -  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn _ =>
    6.31 -    SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)))
    6.32 +  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
    6.33 +    SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
    6.34      "MESON resolution proof procedure";
    6.35  
    6.36  
    6.37  (*** Converting a subgoal into negated conjecture clauses. ***)
    6.38  
    6.39 -val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac];
    6.40 +fun neg_skolemize_tac ctxt =
    6.41 +  EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac ctxt];
    6.42  
    6.43  val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf;
    6.44  
    6.45  fun neg_conjecture_clauses ctxt st0 n =
    6.46    let
    6.47 -    val st = Seq.hd (neg_skolemize_tac n st0)
    6.48 +    val st = Seq.hd (neg_skolemize_tac ctxt n st0)
    6.49      val ({params, prems, ...}, _) = Subgoal.focus (Variable.set_body false ctxt) n st
    6.50    in (neg_clausify prems, map (Term.dest_Free o Thm.term_of o #2) params) end;
    6.51  
    6.52  (*Conversion of a subgoal to conjecture clauses. Each clause has
    6.53    leading !!-bound universal variables, to express generality. *)
    6.54  fun neg_clausify_tac ctxt =
    6.55 -  neg_skolemize_tac THEN'
    6.56 +  neg_skolemize_tac ctxt THEN'
    6.57    SUBGOAL (fn (prop, i) =>
    6.58      let val ts = Logic.strip_assums_hyp prop in
    6.59        EVERY'
     7.1 --- a/src/HOL/ex/Classical.thy	Wed Jul 29 16:43:02 2009 +0200
     7.2 +++ b/src/HOL/ex/Classical.thy	Wed Jul 29 19:36:22 2009 +0200
     7.3 @@ -429,7 +429,7 @@
     7.4  lemma "(\<forall>x y z. R(x,y) & R(y,z) --> R(x,z)) &
     7.5         (\<forall>x. \<exists>y. R(x,y)) -->
     7.6         ~ (\<forall>x. P x = (\<forall>y. R(x,y) --> ~ P y))"
     7.7 -by (tactic{*Meson.safe_best_meson_tac @{claset} 1*})
     7.8 +by (tactic{*Meson.safe_best_meson_tac @{context} 1*})
     7.9      --{*In contrast, @{text meson} is SLOW: 7.6s on griffon*}
    7.10  
    7.11  
    7.12 @@ -723,7 +723,7 @@
    7.13         (\<forall>x y. bird x & snail y \<longrightarrow> ~eats x y) &
    7.14         (\<forall>x. (caterpillar x \<or> snail x) \<longrightarrow> (\<exists>y. plant y & eats x y))
    7.15         \<longrightarrow> (\<exists>x y. animal x & animal y & (\<exists>z. grain z & eats y z & eats x y))"
    7.16 -by (tactic{*Meson.safe_best_meson_tac @{claset} 1*})
    7.17 +by (tactic{*Meson.safe_best_meson_tac @{context} 1*})
    7.18      --{*Nearly twice as fast as @{text meson},
    7.19          which performs iterative deepening rather than best-first search*}
    7.20  
     8.1 --- a/src/HOL/ex/Meson_Test.thy	Wed Jul 29 16:43:02 2009 +0200
     8.2 +++ b/src/HOL/ex/Meson_Test.thy	Wed Jul 29 19:36:22 2009 +0200
     8.3 @@ -31,8 +31,8 @@
     8.4  Goal "(\<exists>x. P x) & (\<forall>x. L x --> ~ (M x & R x)) & (\<forall>x. P x --> (M x & L x)) & ((\<forall>x. P x --> Q x) | (\<exists>x. P x & R x)) --> (\<exists>x. Q x & P x)";
     8.5  by (rtac ccontr 1);
     8.6  val [prem25] = gethyps 1;
     8.7 -val nnf25 = Meson.make_nnf prem25;
     8.8 -val xsko25 = Meson.skolemize nnf25;
     8.9 +val nnf25 = Meson.make_nnf @{context} prem25;
    8.10 +val xsko25 = Meson.skolemize @{context} nnf25;
    8.11  by (cut_facts_tac [xsko25] 1 THEN REPEAT (etac exE 1));
    8.12  val [_,sko25] = gethyps 1;
    8.13  val clauses25 = Meson.make_clauses [sko25];   (*7 clauses*)
    8.14 @@ -51,8 +51,8 @@
    8.15  Goal "((\<exists>x. p x) = (\<exists>x. q x)) & (\<forall>x. \<forall>y. p x & q y --> (r x = s y)) --> ((\<forall>x. p x --> r x) = (\<forall>x. q x --> s x))";
    8.16  by (rtac ccontr 1);
    8.17  val [prem26] = gethyps 1;
    8.18 -val nnf26 = Meson.make_nnf prem26;
    8.19 -val xsko26 = Meson.skolemize nnf26;
    8.20 +val nnf26 = Meson.make_nnf @{context} prem26;
    8.21 +val xsko26 = Meson.skolemize @{context} nnf26;
    8.22  by (cut_facts_tac [xsko26] 1 THEN REPEAT (etac exE 1));
    8.23  val [_,sko26] = gethyps 1;
    8.24  val clauses26 = Meson.make_clauses [sko26];                   (*9 clauses*)
    8.25 @@ -72,8 +72,8 @@
    8.26  Goal "(\<forall>x. \<forall>y. q x y = (\<forall>z. p z x = (p z y::bool))) --> (\<forall>x. (\<forall>y. q x y = (q y x::bool)))";
    8.27  by (rtac ccontr 1);
    8.28  val [prem43] = gethyps 1;
    8.29 -val nnf43 = Meson.make_nnf prem43;
    8.30 -val xsko43 = Meson.skolemize nnf43;
    8.31 +val nnf43 = Meson.make_nnf @{context} prem43;
    8.32 +val xsko43 = Meson.skolemize @{context} nnf43;
    8.33  by (cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1));
    8.34  val [_,sko43] = gethyps 1;
    8.35  val clauses43 = Meson.make_clauses [sko43];   (*6*)
     9.1 --- a/src/Provers/classical.ML	Wed Jul 29 16:43:02 2009 +0200
     9.2 +++ b/src/Provers/classical.ML	Wed Jul 29 19:36:22 2009 +0200
     9.3 @@ -113,8 +113,8 @@
     9.4    val del_context_safe_wrapper: string -> theory -> theory
     9.5    val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
     9.6    val del_context_unsafe_wrapper: string -> theory -> theory
     9.7 -  val get_claset: theory -> claset
     9.8 -  val map_claset: (claset -> claset) -> theory -> theory
     9.9 +  val get_claset: Proof.context -> claset
    9.10 +  val put_claset: claset -> Proof.context -> Proof.context
    9.11    val get_cs: Context.generic -> claset
    9.12    val map_cs: (claset -> claset) -> Context.generic -> Context.generic
    9.13    val safe_dest: int option -> attribute
    9.14 @@ -845,8 +845,8 @@
    9.15      (merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2));
    9.16  );
    9.17  
    9.18 -val get_claset = #1 o GlobalClaset.get;
    9.19 -val map_claset = GlobalClaset.map o apfst;
    9.20 +val get_global_claset = #1 o GlobalClaset.get;
    9.21 +val map_global_claset = GlobalClaset.map o apfst;
    9.22  
    9.23  val get_context_cs = #2 o GlobalClaset.get o ProofContext.theory_of;
    9.24  fun map_context_cs f = GlobalClaset.map (apsnd
    9.25 @@ -871,9 +871,12 @@
    9.26  structure LocalClaset = ProofDataFun
    9.27  (
    9.28    type T = claset;
    9.29 -  val init = get_claset;
    9.30 +  val init = get_global_claset;
    9.31  );
    9.32  
    9.33 +val get_claset = LocalClaset.get;
    9.34 +val put_claset = LocalClaset.put;
    9.35 +
    9.36  fun claset_of ctxt =
    9.37    context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt);
    9.38  
    9.39 @@ -881,13 +884,13 @@
    9.40  (* generic clasets *)
    9.41  
    9.42  val get_cs = Context.cases global_claset_of claset_of;
    9.43 -fun map_cs f = Context.mapping (map_claset f) (LocalClaset.map f);
    9.44 +fun map_cs f = Context.mapping (map_global_claset f) (LocalClaset.map f);
    9.45  
    9.46  
    9.47  (* attributes *)
    9.48  
    9.49  fun attrib f = Thm.declaration_attribute (fn th =>
    9.50 -  Context.mapping (map_claset (f th)) (LocalClaset.map (f th)));
    9.51 +  Context.mapping (map_global_claset (f th)) (LocalClaset.map (f th)));
    9.52  
    9.53  fun safe_dest w = attrib (addSE w o make_elim);
    9.54  val safe_elim = attrib o addSE;