# HG changeset patch
# User wenzelm
# Date 1169208576 -3600
# Node ID 4c53bb6e10e45dfca5308a7cbfde3b994eaa85ef
# Parent  a13299166175007323ff9427bf4fc29c09132fb6
added 'declaration' command;

diff -r a13299166175 -r 4c53bb6e10e4 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Jan 19 13:09:35 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Jan 19 13:09:36 2007 +0100
@@ -306,6 +306,11 @@
     (((P.name -- P.!!! (P.$$$ "=" |-- P.text -- P.text) >> P.triple2))
       >> (Toplevel.theory o Method.method_setup));
 
+val declarationP =
+  OuterSyntax.command "declaration" "generic ML declaration" (K.tag_ml K.thy_decl)
+    (P.opt_locale_target -- P.text
+    >> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt)));
+
 
 (* translation functions *)
 
@@ -923,7 +928,7 @@
   no_syntaxP, translationsP, no_translationsP, axiomsP, defsP,
   constdefsP, definitionP, abbreviationP, notationP, axiomatizationP,
   theoremsP, lemmasP, declareP, globalP, localP, hideP, useP, mlP,
-  ml_commandP, ml_setupP, setupP, method_setupP,
+  ml_commandP, ml_setupP, setupP, method_setupP, declarationP,
   parse_ast_translationP, parse_translationP, print_translationP,
   typed_print_translationP, print_ast_translationP,
   token_translationP, oracleP, contextP, localeP,