src/Pure/Isar/locale.ML
changeset 28927 7e631979922f
parent 28893 4e6fd31c9883
child 28940 df0cb410be35
     1.1 --- a/src/Pure/Isar/locale.ML	Mon Dec 01 12:17:04 2008 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Mon Dec 01 13:43:32 2008 +0100
     1.3 @@ -2043,15 +2043,6 @@
     1.4      Method.intros_tac (wits @ intros) facts st
     1.5    end;
     1.6  
     1.7 -val _ = Context.>> (Context.map_theory
     1.8 -  (Method.add_methods
     1.9 -    [("intro_locales",
    1.10 -      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
    1.11 -      "back-chain introduction rules of locales without unfolding predicates"),
    1.12 -     ("unfold_locales",
    1.13 -      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
    1.14 -      "back-chain all introduction rules of locales")]));
    1.15 -
    1.16  end;
    1.17  
    1.18