diff -r 129db1416717 -r d83797ef0d2d src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/General/path.ML	Mon Nov 28 22:05:32 2011 +0100
@@ -155,7 +155,7 @@
 
 fun pretty path =
   let val s = implode_path path
-  in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end;
+  in Pretty.mark (Isabelle_Markup.path s) (Pretty.str (quote s)) end;
 
 val print = Pretty.str_of o pretty;