cartouche_declaration for Eisbach;

--- a/src/Pure/Isar/args.ML	Sat Mar 07 22:38:11 2015 +0100
+++ b/src/Pure/Isar/args.ML	Sun Mar 08 13:45:11 2015 +0100
@@ -47,6 +47,7 @@
   val named_attribute: (string * Position.T -> morphism -> attribute) ->
     (morphism -> attribute) parser
   val text_declaration: (Input.source -> declaration) -> declaration parser
+  val cartouche_declaration: (Input.source -> declaration) -> declaration parser
   val typ_abbrev: typ context_parser
   val typ: typ context_parser
   val term: term context_parser
@@ -159,6 +160,10 @@
   internal_declaration ||
   text_token >> evaluate Token.Declaration (read o Token.source_position_of);
 
+fun cartouche_declaration read =
+  internal_declaration ||
+  cartouche >> evaluate Token.Declaration (read o Token.source_position_of);
+
 
 (* terms and types *)