| changeset 44615 | a4ff8a787202 |
| parent 44577 | 96b6388d06c4 |
| child 44616 | 4beeaf2a226d |
--- a/src/Pure/Thy/thy_load.scala Thu Sep 01 11:33:44 2011 +0200 +++ b/src/Pure/Thy/thy_load.scala Thu Sep 01 13:34:45 2011 +0200 @@ -11,6 +11,6 @@ def register_thy(thy_name: String) def is_loaded(thy_name: String): Boolean def append(master_dir: String, path: Path): String - def check_thy(node_name: String): Thy_Header + def check_thy(node_name: Document.Node.Name): Thy_Header }