diff -r d61e303fc7e5 -r 3e9809678574 src/Tools/Code/code_printer.ML
--- 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 **)