killed "expand_defs_tac";
it has no raison d'etre now that Skolemization is always done "inline";
the comment in the code suggested that it was used for other things as well but the code clearly did nothing if no Skolem "Frees" were in the problem
--- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML Mon Jun 28 18:02:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML Mon Jun 28 18:08:36 2010 +0200
@@ -1,12 +1,12 @@
(* Title: HOL/Tools/Sledgehammer/meson_tactic.ML
Author: Jia Meng, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
MESON general tactic and proof method.
*)
signature MESON_TACTIC =
sig
- val expand_defs_tac : thm -> tactic
val meson_general_tac : Proof.context -> thm list -> int -> tactic
val setup: theory -> theory
end;
@@ -14,37 +14,11 @@
structure Meson_Tactic : MESON_TACTIC =
struct
-(*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
-fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ _) =
-(* FIXME String.isPrefix Clausifier.skolem_prefix a *) true
- | is_absko _ = false;
-
-fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ _) = (*Definition of Free, not in certain terms*)
- is_Free t andalso not (member (op aconv) xs t)
- | is_okdef _ _ = false
-
-(*This function tries to cope with open locales, which introduce hypotheses of the form
- Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
- of sko_ functions. *)
-fun expand_defs_tac st0 st =
- let val hyps0 = #hyps (rep_thm st0)
- val hyps = #hyps (crep_thm st)
- val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps
- val defs = filter (is_absko o Thm.term_of) newhyps
- val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
- (map Thm.term_of hyps)
- val fixed = OldTerm.term_frees (concl_of st) @
- fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) []
- in Seq.of_list [Local_Defs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
-
-fun meson_general_tac ctxt ths i st0 =
+fun meson_general_tac ctxt ths =
let
val thy = ProofContext.theory_of ctxt
val ctxt0 = Classical.put_claset HOL_cs ctxt
- in
- (Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) ths) i
- THEN expand_defs_tac st0) st0
- end
+ in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) ths) end
val setup =
Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Jun 28 18:02:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Jun 28 18:08:36 2010 +0200
@@ -788,8 +788,7 @@
else
(Meson.MESON (maps neg_clausify)
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
- ctxt i
- THEN Meson_Tactic.expand_defs_tac st0) st0
+ ctxt i) st0
handle ERROR msg => raise METIS ("generic_metis_tac", msg)
end
handle METIS (loc, msg) =>