# HG changeset patch
# User wenzelm
# Date 940941345 -7200
# Node ID 92df50fb89caea106bb836e0f23d82f124b6de4b
# Parent  fa6fec415492fdccfb782625759eb85d98c50d1e
export kill_theory;

diff -r fa6fec415492 -r 92df50fb89ca src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Tue Oct 26 14:35:10 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Tue Oct 26 14:35:45 1999 +0200
@@ -155,6 +155,7 @@
   val add_oracle: (bstring * string) * Comment.text -> theory -> theory
   val begin_theory: string -> string list -> (string * bool) list -> theory
   val end_theory: theory -> theory
+  val kill_theory: string -> unit
   val theory: string * string list * (string * bool) list
     -> Toplevel.transition -> Toplevel.transition
   val context: string -> Toplevel.transition -> Toplevel.transition
@@ -518,16 +519,11 @@
 val begin_theory = gen_begin_theory ThyInfo.begin_theory;
 val begin_update_theory = gen_begin_theory ThyInfo.begin_update_theory;
 
-fun check_known_thy name =
-  ThyInfo.known_thy name orelse (warning ("Lost theory " ^ quote name); false);
-
 fun end_theory thy =
-  if check_known_thy (PureThy.get_name thy) then ThyInfo.end_theory thy
+  if ThyInfo.check_known_thy (PureThy.get_name thy) then ThyInfo.end_theory thy
   else thy;
 
-fun kill_theory thy =
-  let val name = PureThy.get_name thy
-  in if check_known_thy name then ThyInfo.remove_thy name else () end;
+val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy;
 
 
 fun bg_theory (name, parents, files) int =
@@ -535,7 +531,7 @@
 
 fun en_theory thy = (end_theory thy; ());
 
-fun theory spec = Toplevel.init_theory (bg_theory spec) en_theory kill_theory;
+fun theory spec = Toplevel.init_theory (bg_theory spec) en_theory (kill_theory o PureThy.get_name);
 
 
 (* context switch *)