# HG changeset patch
# User haftmann
# Date 1162560166 -3600
# Node ID 0fb5e2123f93f3f4cc1701f3fbd960b85a9f2342
# Parent  7f6bdffe3d06d9b26fbb52c12de845d323f8ba61
tuned

diff -r 7f6bdffe3d06 -r 0fb5e2123f93 src/Pure/Tools/codegen_names.ML
--- a/src/Pure/Tools/codegen_names.ML	Fri Nov 03 14:22:45 2006 +0100
+++ b/src/Pure/Tools/codegen_names.ML	Fri Nov 03 14:22:46 2006 +0100
@@ -25,13 +25,11 @@
   val purify_var: string -> string
   val check_modulename: string -> string
   val has_nsp: string -> string -> bool
-  val nsp_module: string
   val nsp_class: string
   val nsp_tyco: string
   val nsp_inst: string
   val nsp_fun: string
   val nsp_dtco: string
-  val nsp_eval: string
 end;
 
 structure CodegenNames: CODEGEN_NAMES =
@@ -320,13 +318,11 @@
 
 (* shallow name spaces *)
 
-val nsp_module = ""; (*a dummy by convention*)
 val nsp_class = "class";
 val nsp_tyco = "tyco";
 val nsp_inst = "inst";
 val nsp_fun = "fun";
 val nsp_dtco = "dtco";
-val nsp_eval = "EVAL"; (*only for evaluation*)
 
 fun add_nsp shallow name =
   name
diff -r 7f6bdffe3d06 -r 0fb5e2123f93 src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Fri Nov 03 14:22:45 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Fri Nov 03 14:22:46 2006 +0100
@@ -72,7 +72,7 @@
   val merge_code: code * code -> code;
   val project_code: string list (*hidden*) -> string list option (*selected*)
     -> code -> code;
-  val add_eval_def: string (*shallow name space*) * iterm -> code -> string * code;
+  val add_eval_def: string (*bind name*) * iterm -> code -> code;
 
   val ensure_def: (transact -> def * code) -> bool -> string
     -> string -> transact -> transact;
@@ -446,16 +446,10 @@
     |-> (fn x => fn (_, code) => (x, code))
   end;
 
-fun add_eval_def (shallow, e) code =
-  let
-    val name = "VALUE";
-    val sname = NameSpace.pack [shallow, name];
-  in
-    code
-    |> Graph.new_node (sname, Fun ([([], e)], ([("_", [])], ITyVar "_")))
-    |> fold (curry Graph.add_edge sname) (Graph.keys code) (*FIXME*)
-    |> pair name
-  end;
+fun add_eval_def (name, t) code =
+  code
+  |> Graph.new_node (name, Fun ([([], t)], ([("_", [])], ITyVar "_")))
+  |> fold (curry Graph.add_edge name) (Graph.keys code);
 
 
 (** variable name contexts **)