# HG changeset patch
# User wenzelm
# Date 1620913132 -7200
# Node ID caa5a257d3edf6db943bfe1e2f3ded56c06e3dd5
# Parent  8c4ba5f612234e9e05583f4dfb2579dcb1a28caa
unused;

diff -r 8c4ba5f61223 -r caa5a257d3ed src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Wed May 12 17:17:46 2021 +0200
+++ b/src/Pure/Isar/parse.ML	Thu May 13 15:38:52 2021 +0200
@@ -61,7 +61,6 @@
   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: string parser
   val name_range: (string * Position.range) parser
   val name_position: (string * Position.T) parser
@@ -259,8 +258,6 @@
 fun list1 scan = enum1 "," scan;
 fun list scan = enum "," scan;
 
-val properties = $$$ "(" |-- !!! (list (string -- ($$$ "=" |-- string)) --| $$$ ")");
-
 
 (* names and embedded content *)