# HG changeset patch
# User haftmann
# Date 1200901415 -3600
# Node ID ce3cd5f0c4eec47b1c7b1ef18b50a1a8f49d3b70
# Parent  7b8f3a9efa030fda0fef3422b01f2767f5f5051b
tuned

diff -r 7b8f3a9efa03 -r ce3cd5f0c4ee src/Tools/code/code_package.ML
--- a/src/Tools/code/code_package.ML	Mon Jan 21 08:43:34 2008 +0100
+++ b/src/Tools/code/code_package.ML	Mon Jan 21 08:43:35 2008 +0100
@@ -129,7 +129,7 @@
 
 fun satisfies thy t witnesses =
   let
-    fun evl code ((vs, ty), t) deps ct =
+    fun evl code ((vs, ty), t) deps _ =
       CodeTarget.eval_invoke thy ("CodePackage.satisfies_ref", satisfies_ref)
         code (t, ty) witnesses;
   in eval_term thy evl t end;
diff -r 7b8f3a9efa03 -r ce3cd5f0c4ee src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Mon Jan 21 08:43:34 2008 +0100
+++ b/src/Tools/nbe.ML	Mon Jan 21 08:43:35 2008 +0100
@@ -123,11 +123,10 @@
   val name_apps =       prefix ^ "apps";
 in
 
-fun nbe_fun' c = "c_" ^ translate_string (fn "." => "_" | c => c) c;
-val nbe_fun = nbe_fun'; (*FIXME!*)
+fun nbe_fun "" = "nbe_value"
+  | nbe_fun c = "c_" ^ translate_string (fn "." => "_" | c => c) c;
 fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n;
 fun nbe_bound v = "v_" ^ v;
-val nbe_value = "";
 
 (*note: these three are the "turning spots" where proper argument order is established!*)
 fun nbe_apps t [] = t
@@ -136,7 +135,6 @@
 fun nbe_apps_constr c ts =
   name_const `$` ("(" ^ ML_Syntax.print_string c ^ ", " ^ ml_list (rev ts) ^ ")");
 
-
 fun nbe_abss 0 f = f `$` ml_list []
   | nbe_abss n f = name_abs `$$` [string_of_int n, f];
 
@@ -199,7 +197,7 @@
       ([ml_list (rev (dict_args @ map assemble_arg args))], assemble_rhs rhs);
     val default_args = dict_args @ map nbe_bound (Name.invent_list [] "a" ((length o fst o hd) eqns));
     val default_eqn = ([ml_list (rev default_args)], nbe_apps_constr c default_args);
-  in (nbe_fun' c, map assemble_eqn eqns @ [default_eqn]) end;
+  in (nbe_fun c, map assemble_eqn eqns @ [default_eqn]) end;
 
 fun assemble_eqnss gr deps [] = ([], ("", []))
   | assemble_eqnss gr deps eqnss =
@@ -212,7 +210,7 @@
           | NONE => if (is_some o Option.join o try (Graph.get_node gr)) c
               then Global else Constr;
         val deps' = filter (is_some o Option.join o try (Graph.get_node gr)) deps;
-        val bind_deps = ml_list (map nbe_fun' deps');
+        val bind_deps = ml_list (map nbe_fun deps');
         val bind_locals = ml_fundefs (map (assemble_eqns kind) eqnss);
         val result = ml_list (map (fn (c, n) => nbe_abss n (nbe_fun c)) num_args);
         val arg_deps = map (the o Graph.get_node gr) deps';
@@ -279,7 +277,7 @@
     val frees' = map (fn v => Free (v, [])) frees;
     val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs;
   in
-    (nbe_value, (vs, [(map IVar frees, t)]))
+    ("", (vs, [(map IVar frees, t)]))
     |> singleton (compile_eqnss gr deps)
     |> snd
     |> (fn t => apps t (rev (dict_frees @ frees')))