# HG changeset patch
# User wenzelm
# Date 931287814 -7200
# Node ID 29060d9b60d4926262164ba2dca15c146b729bd5
# Parent  020314dadebd7d60452c6a7791fcb6d629773763
begin_theory: disallow finished;

diff -r 020314dadebd -r 29060d9b60d4 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Jul 06 21:03:03 1999 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Jul 06 21:03:34 1999 +0200
@@ -293,6 +293,10 @@
 
 fun begin_theory name parents paths =
   let
+    val _ =
+      if is_some (lookup_thy name) andalso is_finished name then
+        error (loader_msg "cannot change finished theory" [name])
+      else ();
     val _ = (map Path.basic parents; seq weak_use_thy parents);
     val theory = PureThy.begin_theory name (map get_theory parents);
     val _ = change_thys (update_node name parents (init_deps [] [], Some theory));