src/Tools/Code/code_printer.ML

   val first_lower: string -> string
   type var_ctxt
   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
   val Literals: { literal_char: string -> string, literal_string: string -> string,
         literal_numeral: bool -> int -> string,

     val fished2 = map_index (fillup_param x) fished1;
     val (fished3, _) = Name.variants fished2 Name.context;
     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 **)
 
 datatype literals = Literals of {
   literal_char: string -> string,