# HG changeset patch # User wenzelm # Date 1207832008 -7200 # Node ID f9c3c2110b031717a366b8c569e9015e7256e8f3 # Parent 03455add48012cdf038e4d792a96cd29fb14ef4e ThyInfo.get_theory; diff -r 03455add4801 -r f9c3c2110b03 src/Pure/Isar/session.ML --- a/src/Pure/Isar/session.ML Thu Apr 10 14:53:27 2008 +0200 +++ b/src/Pure/Isar/session.ML Thu Apr 10 14:53:28 2008 +0200 @@ -92,7 +92,7 @@ ((fn () => (init reset parent name; Present.init build info doc doc_graph doc_versions (path ()) name - (dumping dump) (get_rpath rpath) verbose (map ThyInfo.theory (ThyInfo.names ())); + (dumping dump) (get_rpath rpath) verbose (map ThyInfo.get_theory (ThyInfo.get_names ())); use root; finish ())) |> setmp_noncritical Proofterm.proofs level