src/Pure/Tools/codegen_names.ML

   fun map_const f = map_names
     (fn (class, tyco, inst, const) => (class, tyco, inst, f const));
 
 end; (*local*)
 
-structure CodegenNamesData = TheoryDataFun
+structure CodeName = TheoryDataFun
 (struct
   val name = "Pure/codegen_names";
   type T = names ref;
   val empty = ref empty_names;
   fun copy (ref names) = ref names;
   val extend = copy;
   fun merge _ (ref names1, ref names2) = ref (merge_names (names1, names2));
   fun print _ _ = ();
 end);
 
-val _ = Context.add_setup CodegenNamesData.init;
+val _ = Context.add_setup CodeName.init;
 
 
 (* forward lookup with cache update *)
 
 fun get thy get_tabs get upd_names upd policy x =
   let
-    val names_ref = CodegenNamesData.get thy
+    val names_ref = CodeName.get thy
     val (Names names) = ! names_ref;
     fun mk_unique used name =
       let
         fun mk_name 0 = name
           | mk_name i = name ^ "_" ^ string_of_int i

 
 (* backward lookup *)
 
 fun rev thy get_tabs errname name =
   let
-    val names_ref = CodegenNamesData.get thy
+    val names_ref = CodeName.get thy
     val (Names names) = ! names_ref;
     val tab = (snd o get_tabs) names;
   in case Symtab.lookup tab name
    of SOME x => x
     | NONE => error ("No such " ^ errname ^ ": " ^ quote name)

     val _ = if (base' = base) andalso forall (op =) (prefix' ~~ prefix)
       then ()
       else
         error ("Name violates naming conventions: " ^ quote name
           ^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base'])))
-    val names_ref = CodegenNamesData.get thy;
+    val names_ref = CodeName.get thy;
     val (Names names) = ! names_ref;
     val (tycotab, tycorev) = #tyco names;
     val _ = if Symtab.defined tycotab tyco
       then error ("Type constructor already named: " ^ quote tyco)
       else ();

     val _ = if (base' = base) andalso forall (op =) (prefix' ~~ prefix)
       then ()
       else
         error ("Name violates naming conventions: " ^ quote name
           ^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base'])))
-    val names_ref = CodegenNamesData.get thy;
+    val names_ref = CodeName.get thy;
     val (Names names) = ! names_ref;
     val (const, constrev) = #const names;
     val c_tys as (c, _) = CodegenConsts.norminst_of_typ thy c_ty;
     val _ = if Consttab.defined const c_tys
       then error ("Constant already named: " ^ quote (CodegenConsts.string_of_const thy c_tys))