| changeset 44159 | 9a35e88d9dc9 |
| parent 43673 | 29eb1cd29961 |
| child 44574 | 24444588fddd |
--- a/src/Pure/Thy/thy_load.scala Fri Aug 12 11:41:26 2011 +0200 +++ b/src/Pure/Thy/thy_load.scala Fri Aug 12 12:03:17 2011 +0200 @@ -10,6 +10,6 @@ { def is_loaded(name: String): Boolean - def check_thy(dir: Path, name: String): (String, Thy_Header.Header) + def check_thy(dir: Path, name: String): (String, Thy_Header) }