src/Pure/Isar/isar_syn.ML
changeset 22088 4c53bb6e10e4
parent 21956 2cbee05b18a1
child 22117 505e040bdcdb
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Jan 19 13:09:35 2007 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Jan 19 13:09:36 2007 +0100
     1.3 @@ -306,6 +306,11 @@
     1.4      (((P.name -- P.!!! (P.$$$ "=" |-- P.text -- P.text) >> P.triple2))
     1.5        >> (Toplevel.theory o Method.method_setup));
     1.6  
     1.7 +val declarationP =
     1.8 +  OuterSyntax.command "declaration" "generic ML declaration" (K.tag_ml K.thy_decl)
     1.9 +    (P.opt_locale_target -- P.text
    1.10 +    >> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt)));
    1.11 +
    1.12  
    1.13  (* translation functions *)
    1.14  
    1.15 @@ -923,7 +928,7 @@
    1.16    no_syntaxP, translationsP, no_translationsP, axiomsP, defsP,
    1.17    constdefsP, definitionP, abbreviationP, notationP, axiomatizationP,
    1.18    theoremsP, lemmasP, declareP, globalP, localP, hideP, useP, mlP,
    1.19 -  ml_commandP, ml_setupP, setupP, method_setupP,
    1.20 +  ml_commandP, ml_setupP, setupP, method_setupP, declarationP,
    1.21    parse_ast_translationP, parse_translationP, print_translationP,
    1.22    typed_print_translationP, print_ast_translationP,
    1.23    token_translationP, oracleP, contextP, localeP,