# HG changeset patch
# User wenzelm
# Date 1283159825 -7200
# Node ID fb9f51ba1bbc856de70ce3141e80ca39c8a835a5
# Parent  7634e3f105764e03149e701f4015930ec52893c8
tuned;

diff -r 7634e3f10576 -r fb9f51ba1bbc src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon Aug 30 11:09:26 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Aug 30 11:17:05 2010 +0200
@@ -44,7 +44,6 @@
   val pwd: Toplevel.transition -> Toplevel.transition
   val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
   val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
-  val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
   val print_context: Toplevel.transition -> Toplevel.transition
   val print_theory: bool -> Toplevel.transition -> Toplevel.transition
   val print_syntax: Toplevel.transition -> Toplevel.transition
@@ -321,11 +320,6 @@
   in File.isabelle_tool "print" ("-c " ^ outfile); () end);
 
 
-(* pretty_setmargin *)
-
-fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.margin_default := n);
-
-
 (* print parts of theory and proof context *)
 
 val print_context = Toplevel.keep Toplevel.print_state_context;
diff -r 7634e3f10576 -r fb9f51ba1bbc src/Pure/Isar/isar_syn.ML
--- 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