src/Pure/Isar/args.ML

   val internal_name: (string * morphism) parser
   val internal_typ: typ parser
   val internal_term: term parser
   val internal_fact: thm list parser
   val internal_attribute: (morphism -> attribute) parser
+  val internal_declaration: declaration parser
   val named_source: (Token.T -> Token.src) -> Token.src parser
   val named_typ: (string -> typ) -> typ parser
   val named_term: (string -> term) -> term parser
   val named_fact: (string -> string option * thm list) -> thm list parser
-  val named_attribute:
-    (string * Position.T -> morphism -> attribute) -> (morphism -> attribute) parser
+  val named_attribute: (string * Position.T -> morphism -> attribute) ->
+    (morphism -> attribute) parser
+  val text_declaration: (Symbol_Pos.source -> declaration) -> declaration parser
   val typ_abbrev: typ context_parser
   val typ: typ context_parser
   val term: term context_parser
   val term_pattern: term context_parser
   val term_abbrev: term context_parser

 val internal_name = value (fn Token.Name a => a);
 val internal_typ = value (fn Token.Typ T => T);
 val internal_term = value (fn Token.Term t => t);
 val internal_fact = value (fn Token.Fact (_, ths) => ths);
 val internal_attribute = value (fn Token.Attribute att => att);
+val internal_declaration = value (fn Token.Declaration decl => decl);
 
 fun named_source read = internal_source || named >> evaluate Token.Source read;
 
 fun named_typ read = internal_typ || named >> evaluate Token.Typ (read o Token.inner_syntax_of);
 fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.inner_syntax_of);

   alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of) >> #2;
 
 fun named_attribute att =
   internal_attribute ||
   named >> evaluate Token.Attribute (fn tok => att (Token.content_of tok, Token.pos_of tok));
+
+fun text_declaration read =
+  internal_declaration ||
+  text_token >> evaluate Token.Declaration (read o Token.source_position_of);
 
 
 (* terms and types *)
 
 val typ_abbrev = Scan.peek (named_typ o Proof_Context.read_typ_abbrev o Context.proof_of);