--- a/src/Pure/Isar/parse.ML	Tue Jul 12 14:54:29 2011 +0200
+++ b/src/Pure/Isar/parse.ML	Tue Jul 12 15:12:50 2011 +0200
@@ -60,6 +60,7 @@
   val and_list1': 'a context_parser -> 'a list context_parser
   val list: 'a parser -> 'a list parser
   val list1: 'a parser -> 'a list parser
+  val properties: Properties.T parser
   val name: bstring parser
   val binding: binding parser
   val xname: xstring parser
@@ -230,6 +231,8 @@
 fun list1 scan = enum1 "," scan;
 fun list scan = enum "," scan;
 
+val properties = $$$ "(" |-- !!! (list (string -- ($$$ "=" |-- string)) --| $$$ ")");
+
 
 (* names and text *)