--- a/src/Pure/Thy/thy_info.scala Mon Jul 04 16:27:11 2011 +0200
+++ b/src/Pure/Thy/thy_info.scala Mon Jul 04 16:51:45 2011 +0200
@@ -12,7 +12,7 @@
/* messages */
private def show_path(names: List[String]): String =
- names.map(Library.quote).mkString(" via ")
+ names.map(quote).mkString(" via ")
private def cycle_msg(names: List[String]): String =
"Cyclic dependency of " + show_path(names)
@@ -45,7 +45,7 @@
catch {
case ERROR(msg) =>
cat_error(msg, "The error(s) above occurred while examining theory " +
- Library.quote(name) + required_by("\n", initiators))
+ quote(name) + required_by("\n", initiators))
}
require_thys(name :: initiators, dir1,
deps + (name -> Exn.Res(text, header)), header.imports)