diff -r ebeb48fd653b -r 81e0368812ad src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Thu Sep 02 12:30:22 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Thu Sep 02 13:43:38 2010 +0200
@@ -70,7 +70,6 @@
   val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
   val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option
 
-
   type tyco_syntax
   type simple_const_syntax
   type complex_const_syntax
@@ -93,10 +92,6 @@
   val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> thm option -> fixity
     -> iterm -> var_ctxt -> Pretty.T * var_ctxt
-
-  val mk_name_module: Name.context -> string option -> (string -> string option)
-    -> 'a Graph.T -> string -> string
-  val dest_name: string -> string * string
 end;
 
 structure Code_Printer : CODE_PRINTER =
@@ -395,28 +390,4 @@
 
 val parse_const_syntax = parse_syntax plain_const_syntax simple_const_syntax fst;
 
-
-(** module name spaces **)
-
-val dest_name =
-  apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
-
-fun mk_name_module reserved module_prefix module_alias program =
-  let
-    fun mk_alias name = case module_alias name
-     of SOME name' => name'
-      | NONE => name
-          |> Long_Name.explode
-          |> map (fn name => (the_single o fst) (Name.variants [name] reserved))
-          |> Long_Name.implode;
-    fun mk_prefix name = case module_prefix
-     of SOME module_prefix => Long_Name.append module_prefix name
-      | NONE => name;
-    val tab =
-      Symtab.empty
-      |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
-           o fst o dest_name o fst)
-             program
-  in the o Symtab.lookup tab end;
-
 end; (*struct*)