# HG changeset patch
# User wenzelm
# Date 1119298459 -7200
# Node ID 7c1cb7ce24eb1235098fa502d1c3a19488df5f76
# Parent  24491bde68dffac546ce408b0cfee0477041ccf7
Theory.begin/end_theory;

diff -r 24491bde68df -r 7c1cb7ce24eb src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Jun 20 22:14:18 2005 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Jun 20 22:14:19 2005 +0200
@@ -420,9 +420,7 @@
     val assert_thy = if upd then quiet_update_thy' true dir else weak_use_thy dir;
     val _ = check_unfinished error name;
     val _ = List.app assert_thy parents;
-    val theory =
-      Context.begin_theory Sign.pp name (map get_theory bparents)
-      |> Sign.local_path;
+    val theory = Theory.begin_theory name (map get_theory bparents);
     val deps =
       if known_thy name then get_deps name
       else (init_deps NONE (map #1 paths));   (*records additional ML files only!*)
@@ -438,7 +436,7 @@
 fun end_theory theory =
   let
     val name = Context.theory_name theory;
-    val theory' = Context.end_theory theory;
+    val theory' = Theory.end_theory theory;
   in put_theory name theory'; theory' end;