1.1 --- a/src/HOL/Tools/meson.ML	Thu Jan 04 17:52:28 2007 +0100
     1.2 +++ b/src/HOL/Tools/meson.ML	Thu Jan 04 17:55:12 2007 +0100
     1.3 @@ -36,7 +36,6 @@
     1.4    val negate_head	: thm -> thm
     1.5    val select_literal	: int -> thm -> thm
     1.6    val skolemize_tac	: int -> tactic
     1.7 -  val make_clauses_tac	: int -> tactic
     1.8  end
     1.9  
    1.10  
    1.11 @@ -646,34 +645,6 @@
    1.12    end
    1.13    handle Subscript => Seq.empty;
    1.14  
    1.15 -(*Top-level conversion to meta-level clauses. Each clause has  
    1.16 -  leading !!-bound universal variables, to express generality. To get 
    1.17 -  meta-clauses instead of disjunctions, uncomment "make_meta_clauses" below.*)
    1.18 -val make_clauses_tac = 
    1.19 -  SUBGOAL
    1.20 -    (fn (prop,_) =>
    1.21 -     let val ts = Logic.strip_assums_hyp prop
    1.22 -     in EVERY1 
    1.23 -	 [METAHYPS
    1.24 -	    (fn hyps => 
    1.25 -              (Method.insert_tac
    1.26 -                (map forall_intr_vars 
    1.27 -                  ( (**make_meta_clauses**) (make_clauses hyps))) 1)),
    1.28 -	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
    1.29 -     end);
    1.30 -     
    1.31 -     
    1.32 -(*** setup the special skoklemization methods ***)
    1.33 -
    1.34 -(*No CHANGED_PROP here, since these always appear in the preamble*)
    1.35 -
    1.36 -val skolemize_setup =
    1.37 -  Method.add_methods
    1.38 -    [("skolemize", Method.no_args (Method.SIMPLE_METHOD' skolemize_tac),
    1.39 -      "Skolemization into existential quantifiers"),
    1.40 -     ("make_clauses", Method.no_args (Method.SIMPLE_METHOD' make_clauses_tac), 
    1.41 -      "Conversion to !!-quantified meta-level clauses")];
    1.42 -
    1.43  end;
    1.44  
    1.45  structure BasicMeson: BASIC_MESON = Meson;