src/HOL/thy_syntax.ML
changeset 3665 3b44fac767f6
parent 3622 85898be702b2
child 3945 ae9c61d69888
     1.1 --- a/src/HOL/thy_syntax.ML	Tue Sep 09 12:09:06 1997 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Wed Sep 10 14:18:12 1997 +0200
     1.3 @@ -122,7 +122,9 @@
     1.4      ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
     1.5      \val thy = ("^tname^"_add_primrec "^tname^"_size_eqns thy)"
     1.6      ,
     1.7 -    "structure " ^ tname ^ " =\n\
     1.8 +    "val _ = deny (" ^ quote tname ^ " mem  map ! (stamps_of_thy thy))\n\
     1.9 +    \   (\"Datatype \\\""^tname^"\\\" would clash with the theory of the same name!\");\n\
    1.10 +    \structure " ^ tname ^ " =\n\
    1.11      \struct\n\
    1.12      \ val inject = map (get_axiom thy) " ^
    1.13          mk_list (map (fn ((s, _), _) => quote ("inject_" ^ strip_quotes s))