src/Pure/Isar/isar_thy.ML
changeset 7932 92df50fb89ca
parent 7909 824ea50b8dbb
child 7953 955fde69fa7b
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Oct 26 14:35:10 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Tue Oct 26 14:35:45 1999 +0200
     1.3 @@ -155,6 +155,7 @@
     1.4    val add_oracle: (bstring * string) * Comment.text -> theory -> theory
     1.5    val begin_theory: string -> string list -> (string * bool) list -> theory
     1.6    val end_theory: theory -> theory
     1.7 +  val kill_theory: string -> unit
     1.8    val theory: string * string list * (string * bool) list
     1.9      -> Toplevel.transition -> Toplevel.transition
    1.10    val context: string -> Toplevel.transition -> Toplevel.transition
    1.11 @@ -518,16 +519,11 @@
    1.12  val begin_theory = gen_begin_theory ThyInfo.begin_theory;
    1.13  val begin_update_theory = gen_begin_theory ThyInfo.begin_update_theory;
    1.14  
    1.15 -fun check_known_thy name =
    1.16 -  ThyInfo.known_thy name orelse (warning ("Lost theory " ^ quote name); false);
    1.17 -
    1.18  fun end_theory thy =
    1.19 -  if check_known_thy (PureThy.get_name thy) then ThyInfo.end_theory thy
    1.20 +  if ThyInfo.check_known_thy (PureThy.get_name thy) then ThyInfo.end_theory thy
    1.21    else thy;
    1.22  
    1.23 -fun kill_theory thy =
    1.24 -  let val name = PureThy.get_name thy
    1.25 -  in if check_known_thy name then ThyInfo.remove_thy name else () end;
    1.26 +val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy;
    1.27  
    1.28  
    1.29  fun bg_theory (name, parents, files) int =
    1.30 @@ -535,7 +531,7 @@
    1.31  
    1.32  fun en_theory thy = (end_theory thy; ());
    1.33  
    1.34 -fun theory spec = Toplevel.init_theory (bg_theory spec) en_theory kill_theory;
    1.35 +fun theory spec = Toplevel.init_theory (bg_theory spec) en_theory (kill_theory o PureThy.get_name);
    1.36  
    1.37  
    1.38  (* context switch *)