# HG changeset patch
# User blanchet
# Date 1277741316 -7200
# Node ID bcb19259f92a8a07e19138c2659dec0f5a22a2de
# Parent  fa57a87f92a0c527fbb37bb8939f5bb632f62143
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

diff -r fa57a87f92a0 -r bcb19259f92a src/HOL/Tools/Sledgehammer/meson_tactic.ML
--- 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 =>
diff -r fa57a87f92a0 -r bcb19259f92a src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- 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) =>