src/Pure/Isar/class_target.ML
changeset 30510 4120fc59dd85
parent 30364 577edc39b501
child 30515 bca05b17b618
     1.1 --- a/src/Pure/Isar/class_target.ML	Fri Mar 13 19:53:09 2009 +0100
     1.2 +++ b/src/Pure/Isar/class_target.ML	Fri Mar 13 19:58:26 2009 +0100
     1.3 @@ -616,9 +616,9 @@
     1.4  
     1.5  val _ = Context.>> (Context.map_theory
     1.6    (Method.add_methods
     1.7 -   [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
     1.8 +   [("intro_classes", Method.no_args (METHOD intro_classes_tac),
     1.9        "back-chain introduction rules of classes"),
    1.10 -    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
    1.11 +    ("default", Method.thms_ctxt_args (METHOD oo default_tac),
    1.12        "apply some intro/elim rule")]));
    1.13  
    1.14  end;