# HG changeset patch
# User wenzelm
# Date 1208442645 -7200
# Node ID 493db7848904c4697ca29c798b2125aa292359bb
# Parent  6c7e4d858bae3d0331ed8754ef872c9bbc361df4
Pretty.mark;

diff -r 6c7e4d858bae -r 493db7848904 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Apr 17 11:40:00 2008 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Apr 17 16:30:45 2008 +0200
@@ -43,12 +43,12 @@
 (* diagnostics *)
 
 fun report_keyword name =
-  Pretty.markup (Markup.keyword_decl name)
-    [Pretty.str ("Outer syntax keyword: " ^ quote name)];
+  Pretty.mark (Markup.keyword_decl name)
+    (Pretty.str ("Outer syntax keyword: " ^ quote name));
 
 fun report_command name kind =
-  Pretty.markup (Markup.command_decl name kind)
-    [Pretty.str ("Outer syntax command: " ^ quote name ^ " (" ^ kind ^ ")")];
+  Pretty.mark (Markup.command_decl name kind)
+    (Pretty.str ("Outer syntax command: " ^ quote name ^ " (" ^ kind ^ ")"));
 
 
 (* parsers *)
diff -r 6c7e4d858bae -r 493db7848904 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Thu Apr 17 11:40:00 2008 +0200
+++ b/src/Pure/codegen.ML	Thu Apr 17 16:30:45 2008 +0200
@@ -1018,7 +1018,7 @@
           NONE => state
         | SOME NONE => state
         | SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
-            Pretty.markup Markup.hilite [pretty_counterex ctxt cex]]) state
+            Pretty.mark Markup.hilite (pretty_counterex ctxt cex)]) state
       end handle TimeLimit.TimeOut => (warning "Auto quickcheck: timeout."; state);
   in
     if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)