changeset 26053 | f8ee5cbb3068 |
parent 25956 | dae57244f1c7 |
child 26070 | 21b78307096f |
--- a/src/Pure/Isar/isar_cmd.ML Sun Feb 10 20:49:46 2008 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Sun Feb 10 20:49:47 2008 +0100 @@ -392,7 +392,7 @@ (* nested commands *) fun nested_command props (str, pos) = - let val pos' = Position.of_properties (props @ Position.properties_of pos) in + let val pos' = Position.of_properties (props |> Position.default_properties pos) in (case OuterSyntax.parse pos' str of [transition] => transition | _ => error "exactly one command expected")