src/Pure/Isar/isar_syn.ML
changeset 43775 b361c7d184e7
parent 43227 359c190ede75
child 43947 9b00f09f7721
--- a/src/Pure/Isar/isar_syn.ML	Tue Jul 12 14:54:29 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jul 12 15:12:50 2011 +0200
@@ -766,7 +766,7 @@
 (* nested commands *)
 
 val props_text =
-  Scan.optional Parse_Value.properties [] -- Parse.position Parse.string
+  Scan.optional Parse.properties [] -- Parse.position Parse.string
   >> (fn (props, (str, pos)) =>
       (Position.of_properties (Position.default_properties pos props), str));