src/Pure/Isar/isar_cmd.ML
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")