--- 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*)