src/Pure/Isar/class_target.ML
changeset 30521 3ec2d35b380f
parent 30519 c05c0199826f
parent 30515 bca05b17b618
child 30764 3e3e7aa0cc7a
     1.1 --- a/src/Pure/Isar/class_target.ML	Fri Mar 13 19:18:07 2009 +0100
     1.2 +++ b/src/Pure/Isar/class_target.ML	Fri Mar 13 23:56:07 2009 +0100
     1.3 @@ -615,11 +615,10 @@
     1.4      default_intro_tac ctxt facts;
     1.5  
     1.6  val _ = Context.>> (Context.map_theory
     1.7 -  (Method.add_methods
     1.8 -   [("intro_classes", Method.no_args (Method.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 -      "apply some intro/elim rule")]));
    1.12 + (Method.setup (Binding.name "intro_classes") (Scan.succeed (K (METHOD intro_classes_tac)))
    1.13 +    "back-chain introduction rules of classes" #>
    1.14 +  Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac))
    1.15 +    "apply some intro/elim rule"));
    1.16  
    1.17  end;
    1.18