src/Pure/Thy/thy_header.scala
changeset 43652 dcd0b667f73d
parent 43648 e32de528b5ef
child 43661 39fdbd814c7f
     1.1 --- a/src/Pure/Thy/thy_header.scala	Mon Jul 04 16:27:11 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Mon Jul 04 16:51:45 2011 +0200
     1.3 @@ -119,6 +119,6 @@
     1.4      val header = read(source)
     1.5      val name1 = header.name
     1.6      if (name == name1) header
     1.7 -    else error("Bad file name " + Thy_Header.thy_path(name) + " for theory " + Library.quote(name1))
     1.8 +    else error("Bad file name " + Thy_Header.thy_path(name) + " for theory " + quote(name1))
     1.9    }
    1.10  }