--- a/src/Tools/Code/code_printer.ML Mon Oct 12 14:22:54 2009 +0200
+++ b/src/Tools/Code/code_printer.ML Mon Oct 12 15:46:38 2009 +0200
@@ -27,6 +27,8 @@
val make_vars: string list -> var_ctxt
val intro_vars: string list -> var_ctxt -> var_ctxt
val lookup_var: var_ctxt -> string -> string
+ val intro_base_names: (string -> bool) -> (string -> string)
+ -> string list -> var_ctxt -> var_ctxt
val aux_params: var_ctxt -> iterm list list -> string list
type literals
@@ -134,6 +136,13 @@
val vars' = intro_vars fished3 vars;
in map (lookup_var vars') fished3 end;
+fun intro_base_names no_syntax deresolve names = names
+ |> map_filter (fn name => if no_syntax name then
+ let val name' = deresolve name in
+ if Long_Name.is_qualified name' then NONE else SOME name'
+ end else NONE)
+ |> intro_vars;
+
(** pretty literals **)