author | wenzelm |
Thu, 24 Jan 2008 23:51:17 +0100 | |
changeset 25956 | dae57244f1c7 |
parent 25955 | 94a515ed8a39 |
child 25957 | 2cfb703fa8d8 |
--- a/src/Pure/Isar/isar_cmd.ML Thu Jan 24 23:51:15 2008 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Thu Jan 24 23:51:17 2008 +0100 @@ -394,7 +394,7 @@ fun nested_command props (str, pos) = let val pos' = Position.of_properties (props @ Position.properties_of pos) in (case OuterSyntax.parse pos' str of - [transition] => Toplevel.properties props transition + [transition] => transition | _ => error "exactly one command expected") end;