Theory.begin/end_theory;
authorwenzelm
Mon Jun 20 22:14:19 2005 +0200 (2005-06-20)
changeset 165047c1cb7ce24eb
parent 16503 24491bde68df
child 16505 c4b2e3cd84ab
Theory.begin/end_theory;
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Mon Jun 20 22:14:18 2005 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Mon Jun 20 22:14:19 2005 +0200
     1.3 @@ -420,9 +420,7 @@
     1.4      val assert_thy = if upd then quiet_update_thy' true dir else weak_use_thy dir;
     1.5      val _ = check_unfinished error name;
     1.6      val _ = List.app assert_thy parents;
     1.7 -    val theory =
     1.8 -      Context.begin_theory Sign.pp name (map get_theory bparents)
     1.9 -      |> Sign.local_path;
    1.10 +    val theory = Theory.begin_theory name (map get_theory bparents);
    1.11      val deps =
    1.12        if known_thy name then get_deps name
    1.13        else (init_deps NONE (map #1 paths));   (*records additional ML files only!*)
    1.14 @@ -438,7 +436,7 @@
    1.15  fun end_theory theory =
    1.16    let
    1.17      val name = Context.theory_name theory;
    1.18 -    val theory' = Context.end_theory theory;
    1.19 +    val theory' = Theory.end_theory theory;
    1.20    in put_theory name theory'; theory' end;
    1.21  
    1.22