src/Pure/Tools/codegen_thingol.ML

   val get_def: module -> string -> def;
   val merge_module: module * module -> module;
   val diff_module: module * module -> (string * def) list;
   val project_module: string list -> module -> module;
   val purge_module: string list -> module -> module;
-  val add_eval_def: iterm -> module -> string * module;
+  val add_eval_def: string (*shallow name space*) * iterm -> module -> string * module;
   val delete_garbage: string list (*hidden definitions*) -> module -> module;
   val has_nsp: string -> string -> bool;
   val ensure_def: (string -> transact -> def transact_fin) -> bool -> string
     -> string -> transact -> transact;
   val succeed: 'a -> transact -> 'a transact_fin;

     val _ = (writeln o cat_lines o map (fn (x, y) => x ^ " -> " ^ y)) adddeps;*)
   in
     empty_module
     |> fold (fn name => add_def (name, get_def modl name)) selected
 (*     |> fold ensure_bot (hidden @ bots')  *)
-    |> fold (fn (x, y) => (writeln ("adding " ^ x ^ " -> " ^ y); add_dep (x, y))) adddeps
+    |> fold (fn (x, y) => ((*writeln ("adding " ^ x ^ " -> " ^ y);*) add_dep (x, y))) adddeps
   end;
 
 fun allimports_of modl =
   let
     fun imps_of prfx (Module modl) imps tab =

     |> pair init
     |> handle_fail f
     |-> (fn x => fn (_, modl) => (x, modl))
   end;
 
-fun add_eval_def e modl =
-  let
-    val name = hd (Name.invent_list (Graph.keys modl) "VALUE" 1);
+fun add_eval_def (shallow, e) modl =
+  let
+    val name = "VALUE";
+    val sname = NameSpace.pack [shallow, name];
   in
     modl
-    |> add_def (name, Fun ([([], e)], ([], "" `%% [])))
-    |> fold (curry add_dep name) (add_deps_of_term e [])
+    |> add_def (sname, Fun ([([], e)], ([("a", [])], ITyVar "a")))
+    |> fold (curry add_dep sname) (add_deps_of_term e [])
     |> pair name
   end;
 
 
 (** generic serialization **)