# HG changeset patch
# User wenzelm
# Date 940525165 -7200
# Node ID 824ea50b8dbb62e872836ff892a9c8bb91c1d0df
# Parent  0b191b36ad9724c8bf263189eb97d18c37066d50
end/kill_theory: check_known_thy;

diff -r 0b191b36ad97 -r 824ea50b8dbb src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Thu Oct 21 18:59:01 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Thu Oct 21 18:59:25 1999 +0200
@@ -517,8 +517,17 @@
 
 val begin_theory = gen_begin_theory ThyInfo.begin_theory;
 val begin_update_theory = gen_begin_theory ThyInfo.begin_update_theory;
-val end_theory = ThyInfo.end_theory;
-fun kill_theory thy = ThyInfo.remove_thy (PureThy.get_name thy);
+
+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
+  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;
 
 
 fun bg_theory (name, parents, files) int =