# HG changeset patch
# User nipkow
# Date 873893892 -7200
# Node ID 3b44fac767f684938ee1552b299fbcf48915dd8b
# Parent  2dced1ac2d8e8fb90389a007daedbe905fbfdaf3
Added Larry's test for preventing a datatype shadowing a theory.

diff -r 2dced1ac2d8e -r 3b44fac767f6 src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Tue Sep 09 12:09:06 1997 +0200
+++ b/src/HOL/thy_syntax.ML	Wed Sep 10 14:18:12 1997 +0200
@@ -122,7 +122,9 @@
     ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
     \val thy = ("^tname^"_add_primrec "^tname^"_size_eqns thy)"
     ,
-    "structure " ^ tname ^ " =\n\
+    "val _ = deny (" ^ quote tname ^ " mem  map ! (stamps_of_thy thy))\n\
+    \   (\"Datatype \\\""^tname^"\\\" would clash with the theory of the same name!\");\n\
+    \structure " ^ tname ^ " =\n\
     \struct\n\
     \ val inject = map (get_axiom thy) " ^
         mk_list (map (fn ((s, _), _) => quote ("inject_" ^ strip_quotes s))