1.1 --- a/src/HOL/Tools/meson.ML	Wed Nov 29 15:44:46 2006 +0100
     1.2 +++ b/src/HOL/Tools/meson.ML	Wed Nov 29 15:44:51 2006 +0100
     1.3 @@ -666,15 +666,11 @@
     1.4  
     1.5  (*No CHANGED_PROP here, since these always appear in the preamble*)
     1.6  
     1.7 -val skolemize_meth = Method.SIMPLE_METHOD' HEADGOAL skolemize_tac;
     1.8 -
     1.9 -val make_clauses_meth = Method.SIMPLE_METHOD' HEADGOAL make_clauses_tac;
    1.10 -
    1.11  val skolemize_setup =
    1.12    Method.add_methods
    1.13 -    [("skolemize", Method.no_args skolemize_meth, 
    1.14 +    [("skolemize", Method.no_args (Method.SIMPLE_METHOD' skolemize_tac),
    1.15        "Skolemization into existential quantifiers"),
    1.16 -     ("make_clauses", Method.no_args make_clauses_meth, 
    1.17 +     ("make_clauses", Method.no_args (Method.SIMPLE_METHOD' make_clauses_tac), 
    1.18        "Conversion to !!-quantified meta-level clauses")];
    1.19  
    1.20  end;