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));