unused;
authorwenzelm
Thu, 13 May 2021 15:38:52 +0200
changeset 73689 caa5a257d3ed
parent 73688 8c4ba5f61223
child 73690 9267a04aabe6
unused;
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 *)