# HG changeset patch
# User haftmann
# Date 1292940955 -3600
# Node ID aaf5968c67efda6bfc5e8179a72da27a09d86524
# Parent  e82fc600a3a5df39fdb7ca1231dc61f15329c149
tuned names

diff -r e82fc600a3a5 -r aaf5968c67ef src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Tue Dec 21 10:20:33 2010 +0100
+++ b/src/Tools/Code/code_target.ML	Tue Dec 21 15:15:55 2010 +0100
@@ -410,7 +410,7 @@
     else Isabelle_System.with_tmp_dir "Code_Test" (ext_check env_param)
   end;
 
-fun evaluation mounted_serializer prepared_program deps ((vs, ty), t) =
+fun evaluation mounted_serializer prepared_program consts ((vs, ty), t) =
   let
     val _ = if Code_Thingol.contains_dict_var t then
       error "Term to be evaluated contains free dictionaries" else ();
@@ -421,16 +421,16 @@
     val program = prepared_program
       |> Graph.new_node (value_name,
           Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
-      |> fold (curry (perhaps o try o Graph.add_edge) value_name) deps;
+      |> fold (curry (perhaps o try o Graph.add_edge) value_name) consts;
     val (program_code, deresolve) = produce (mounted_serializer program);
     val value_name' = the (deresolve value_name);
   in (program_code, value_name') end;
 
-fun evaluator thy target naming program deps =
+fun evaluator thy target naming program consts =
   let
     val (mounted_serializer, prepared_program) = mount_serializer thy
-      target NONE "Code" [] naming program deps;
-  in evaluation mounted_serializer prepared_program deps end;
+      target NONE "Code" [] naming program consts;
+  in evaluation mounted_serializer prepared_program consts end;
 
 end; (* local *)