# HG changeset patch
# User wenzelm
# Date 1201215077 -3600
# Node ID dae57244f1c7f32e8e6a034c76121c01a292b246
# Parent  94a515ed8a39d21ec198ce2f72228bd078811a3f
removed unused Toplevel.properties;

diff -r 94a515ed8a39 -r dae57244f1c7 src/Pure/Isar/isar_cmd.ML
--- 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;