src/Pure/Isar/isar_thy.ML
changeset 7909 824ea50b8dbb
parent 7862 3e75fbd4a46b
child 7932 92df50fb89ca
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Oct 21 18:59:01 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Oct 21 18:59:25 1999 +0200
     1.3 @@ -517,8 +517,17 @@
     1.4  
     1.5  val begin_theory = gen_begin_theory ThyInfo.begin_theory;
     1.6  val begin_update_theory = gen_begin_theory ThyInfo.begin_update_theory;
     1.7 -val end_theory = ThyInfo.end_theory;
     1.8 -fun kill_theory thy = ThyInfo.remove_thy (PureThy.get_name thy);
     1.9 +
    1.10 +fun check_known_thy name =
    1.11 +  ThyInfo.known_thy name orelse (warning ("Lost theory " ^ quote name); false);
    1.12 +
    1.13 +fun end_theory thy =
    1.14 +  if check_known_thy (PureThy.get_name thy) then ThyInfo.end_theory thy
    1.15 +  else thy;
    1.16 +
    1.17 +fun kill_theory thy =
    1.18 +  let val name = PureThy.get_name thy
    1.19 +  in if check_known_thy name then ThyInfo.remove_thy name else () end;
    1.20  
    1.21  
    1.22  fun bg_theory (name, parents, files) int =