| changeset 63806 | c54a53ef1873 |
| parent 62808 | 288c309df28d |
| child 63933 | e149e3e320a3 |
--- a/src/Pure/Syntax/syntax_ext.ML Mon Sep 05 22:09:52 2016 +0200 +++ b/src/Pure/Syntax/syntax_ext.ML Mon Sep 05 23:11:00 2016 +0200 @@ -183,8 +183,8 @@ in props end; val get_string = get_property "" I; -val get_bool = get_property false Markup.parse_bool; -val get_nat = get_property 0 Markup.parse_nat; +val get_bool = get_property false Value.parse_bool; +val get_nat = get_property 0 Value.parse_nat; end;