1.1 --- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML	Mon Jun 28 18:02:36 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/meson_tactic.ML	Mon Jun 28 18:08:36 2010 +0200
     1.3 @@ -1,12 +1,12 @@
     1.4  (*  Title:      HOL/Tools/Sledgehammer/meson_tactic.ML
     1.5      Author:     Jia Meng, Cambridge University Computer Laboratory
     1.6 +    Author:     Jasmin Blanchette, TU Muenchen
     1.7  
     1.8  MESON general tactic and proof method.
     1.9  *)
    1.10  
    1.11  signature MESON_TACTIC =
    1.12  sig
    1.13 -  val expand_defs_tac : thm -> tactic
    1.14    val meson_general_tac : Proof.context -> thm list -> int -> tactic
    1.15    val setup: theory -> theory
    1.16  end;
    1.17 @@ -14,37 +14,11 @@
    1.18  structure Meson_Tactic : MESON_TACTIC =
    1.19  struct
    1.20  
    1.21 -(*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
    1.22 -fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ _) =
    1.23 -(*  FIXME  String.isPrefix Clausifier.skolem_prefix a *) true
    1.24 -  | is_absko _ = false;
    1.25 -
    1.26 -fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ _) =   (*Definition of Free, not in certain terms*)
    1.27 -      is_Free t andalso not (member (op aconv) xs t)
    1.28 -  | is_okdef _ _ = false
    1.29 -
    1.30 -(*This function tries to cope with open locales, which introduce hypotheses of the form
    1.31 -  Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
    1.32 -  of sko_ functions. *)
    1.33 -fun expand_defs_tac st0 st =
    1.34 -  let val hyps0 = #hyps (rep_thm st0)
    1.35 -      val hyps = #hyps (crep_thm st)
    1.36 -      val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps
    1.37 -      val defs = filter (is_absko o Thm.term_of) newhyps
    1.38 -      val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
    1.39 -                                      (map Thm.term_of hyps)
    1.40 -      val fixed = OldTerm.term_frees (concl_of st) @
    1.41 -                  fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) []
    1.42 -  in Seq.of_list [Local_Defs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
    1.43 -
    1.44 -fun meson_general_tac ctxt ths i st0 =
    1.45 +fun meson_general_tac ctxt ths =
    1.46    let
    1.47      val thy = ProofContext.theory_of ctxt
    1.48      val ctxt0 = Classical.put_claset HOL_cs ctxt
    1.49 -  in
    1.50 -    (Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) ths) i
    1.51 -     THEN expand_defs_tac st0) st0
    1.52 -  end
    1.53 +  in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) ths) end
    1.54  
    1.55  val setup =
    1.56    Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>

     2.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Jun 28 18:02:36 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Jun 28 18:08:36 2010 +0200
     2.3 @@ -788,8 +788,7 @@
     2.4      else
     2.5        (Meson.MESON (maps neg_clausify)
     2.6                     (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
     2.7 -                   ctxt i
     2.8 -       THEN Meson_Tactic.expand_defs_tac st0) st0
     2.9 +                   ctxt i) st0
    2.10       handle ERROR msg => raise METIS ("generic_metis_tac", msg)
    2.11    end
    2.12    handle METIS (loc, msg) =>