1.1 --- a/src/Pure/Thy/present.ML	Tue Nov 18 18:25:42 2008 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Tue Nov 18 18:25:45 2008 +0100
     1.3 @@ -89,7 +89,7 @@
     1.4  fun write_graph gr path =
     1.5    File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
     1.6      "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
     1.7 -    path ^ "\" > " ^ space_implode " " (map Library.quote parents) ^ " ;") gr));
     1.8 +    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
     1.9  
    1.10  fun display_graph gr =
    1.11    let