# HG changeset patch # User wenzelm # Date 1536345318 -7200 # Node ID 7a420bee1eeab7e569f5786905764a2ec28c9d99 # Parent f50d98a0e14084a845b779d549eb8e48def2cdc7 tuned signature; diff -r f50d98a0e140 -r 7a420bee1eea src/Pure/Thy/thy_resources.scala --- a/src/Pure/Thy/thy_resources.scala Fri Sep 07 20:15:17 2018 +0200 +++ b/src/Pure/Thy/thy_resources.scala Fri Sep 07 20:35:18 2018 +0200 @@ -386,7 +386,7 @@ copy(theories = theories -- remove) } - lazy val theories_graph: Graph[Document.Node.Name, Unit] = + lazy val theory_graph: Graph[Document.Node.Name, Unit] = { val entries = for ((name, theory) <- theories.toList) @@ -463,7 +463,7 @@ { state.change_result(st => { - val graph = st.theories_graph + val graph = st.theory_graph val all_nodes = graph.topological_order val purge =