changeset 56208 | 06cc31dff138 |
parent 56206 | 7adec2a527f5 |
child 56210 | c7c85cdb725d |
--- a/src/Pure/ROOT.ML Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Pure/ROOT.ML Tue Mar 18 17:39:03 2014 +0100 @@ -281,7 +281,7 @@ use "Thy/present.ML"; use "PIDE/command.ML"; use "PIDE/query_operation.ML"; -use "Thy/thy_load.ML"; +use "PIDE/resources.ML"; use "Thy/thy_info.ML"; use "PIDE/document.ML";