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