# HG changeset patch
# User skalberg
# Date 1080742253 -7200
# Node ID 255ad604e08e4c8c9be0039ec9d85f47289a02a8
# Parent  0c135fa75626f185afab79707dd82d9bd38a52c3
Added check that Theory.ML does not occur in the files section of the theory
Theory.

diff -r 0c135fa75626 -r 255ad604e08e NEWS
--- a/NEWS	Wed Mar 31 11:02:00 2004 +0200
+++ b/NEWS	Wed Mar 31 16:10:53 2004 +0200
@@ -45,6 +45,11 @@
   later.  It is useful for constants whose behaviour is fixed axiomatically
   rather than definitionally, such as the meta-logic connectives.
 
+* Pure: It is now illegal to specify Theory.ML explicitly as a dependency
+  in the files section of the theory Theory. (This is more of a diagnostic
+  than a restriction, as the theory loader screws up if Theory.ML is manually
+  loaded.)
+
 *** Isar ***
 
 * Tactic emulation methods ?rule_tac, cut_tac, subgoal_tac and thin_tac:
diff -r 0c135fa75626 -r 255ad604e08e src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Wed Mar 31 11:02:00 2004 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Wed Mar 31 16:10:53 2004 +0200
@@ -577,7 +577,11 @@
 (* theory init and exit *)
 
 fun gen_begin_theory upd name parents files =
-  ThyInfo.begin_theory Present.begin_theory upd name parents (map (apfst Path.unpack) files);
+  let val ml_filename = Path.pack (ThyLoad.ml_path name);
+      val () = if exists (equal ml_filename o #1) files
+               then error ((quote ml_filename) ^ " not allowed in files section for theory " ^ name)
+               else ()
+  in ThyInfo.begin_theory Present.begin_theory upd name parents (map (apfst Path.unpack) files) end;
 
 val begin_theory = gen_begin_theory false;