1.1 --- a/src/Pure/Isar/locale.ML	Fri Mar 13 19:53:09 2009 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Fri Mar 13 19:58:26 2009 +0100
     1.3 @@ -489,10 +489,10 @@
     1.4  val _ = Context.>> (Context.map_theory
     1.5    (Method.add_methods
     1.6      [("intro_locales",
     1.7 -      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
     1.8 +      Method.ctxt_args (fn ctxt => METHOD (intro_locales_tac false ctxt)),
     1.9        "back-chain introduction rules of locales without unfolding predicates"),
    1.10       ("unfold_locales",
    1.11 -      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
    1.12 +      Method.ctxt_args (fn ctxt => METHOD (intro_locales_tac true ctxt)),
    1.13        "back-chain all introduction rules of locales")]));
    1.14  
    1.15  end;