# HG changeset patch
# User haftmann
# Date 1166426497 -3600
# Node ID 0ce06e95982ad5ded6d855dd2c8e7d9a0dd48dc4
# Parent  a3efbae45735ef3a30515ec3c5c3de70692ab054
introduces "__" naming policy

diff -r a3efbae45735 -r 0ce06e95982a src/Pure/Tools/codegen_names.ML
--- a/src/Pure/Tools/codegen_names.ML	Mon Dec 18 08:21:35 2006 +0100
+++ b/src/Pure/Tools/codegen_names.ML	Mon Dec 18 08:21:37 2006 +0100
@@ -147,6 +147,11 @@
       else NONE;
   in case thy_of thy
    of SOME thy => Context.theory_name thy
+        |> explode
+        (*should disappear as soon as hierarchical theory name spaces are available*)
+        |> Symbol.scanner "Malformed name"
+             (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.not_eof))
+        |> implode
     | NONE => error (errmsg x) end;
 
 fun thyname_of_class thy =