src/Pure/Isar/isar_syn.ML
changeset 38870 fb9f51ba1bbc
parent 38708 8915e3ce8655
child 38888 8248cda328de
--- a/src/Pure/Isar/isar_syn.ML	Mon Aug 30 11:09:26 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Aug 30 11:17:05 2010 +0200
@@ -786,7 +786,8 @@
 
 val _ =
   Outer_Syntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
-    Keyword.diag (Parse.nat >> (Toplevel.no_timing oo Isar_Cmd.pretty_setmargin));
+    Keyword.diag (Parse.nat >>
+      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Pretty.margin_default := n)));
 
 val _ =
   Outer_Syntax.improper_command "help" "print outer syntax commands" Keyword.diag