src/HOL/Tools/meson.ML
changeset 18708 4b3dadb4fe33
parent 18680 677e2bdd75f0
child 18752 c9c6ae9e8b88
     1.1 --- a/src/HOL/Tools/meson.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/HOL/Tools/meson.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -590,11 +590,11 @@
     1.4  val make_clauses_meth = Method.SIMPLE_METHOD' HEADGOAL make_clauses_tac;
     1.5  
     1.6  val skolemize_setup =
     1.7 - [Method.add_methods
     1.8 -  [("skolemize", Method.no_args skolemize_meth, 
     1.9 -    "Skolemization into existential quantifiers"),
    1.10 -   ("make_clauses", Method.no_args make_clauses_meth, 
    1.11 -    "Conversion to !!-quantified meta-level clauses")]];
    1.12 +  Method.add_methods
    1.13 +    [("skolemize", Method.no_args skolemize_meth, 
    1.14 +      "Skolemization into existential quantifiers"),
    1.15 +     ("make_clauses", Method.no_args make_clauses_meth, 
    1.16 +      "Conversion to !!-quantified meta-level clauses")];
    1.17  
    1.18  end;
    1.19