tuned names
authorhaftmann
Tue Dec 21 15:15:55 2010 +0100 (2010-12-21)
changeset 41364aaf5968c67ef
parent 41351 e82fc600a3a5
child 41365 54dfe5c584e8
tuned names
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_target.ML	Tue Dec 21 10:20:33 2010 +0100
     1.2 +++ b/src/Tools/Code/code_target.ML	Tue Dec 21 15:15:55 2010 +0100
     1.3 @@ -410,7 +410,7 @@
     1.4      else Isabelle_System.with_tmp_dir "Code_Test" (ext_check env_param)
     1.5    end;
     1.6  
     1.7 -fun evaluation mounted_serializer prepared_program deps ((vs, ty), t) =
     1.8 +fun evaluation mounted_serializer prepared_program consts ((vs, ty), t) =
     1.9    let
    1.10      val _ = if Code_Thingol.contains_dict_var t then
    1.11        error "Term to be evaluated contains free dictionaries" else ();
    1.12 @@ -421,16 +421,16 @@
    1.13      val program = prepared_program
    1.14        |> Graph.new_node (value_name,
    1.15            Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
    1.16 -      |> fold (curry (perhaps o try o Graph.add_edge) value_name) deps;
    1.17 +      |> fold (curry (perhaps o try o Graph.add_edge) value_name) consts;
    1.18      val (program_code, deresolve) = produce (mounted_serializer program);
    1.19      val value_name' = the (deresolve value_name);
    1.20    in (program_code, value_name') end;
    1.21  
    1.22 -fun evaluator thy target naming program deps =
    1.23 +fun evaluator thy target naming program consts =
    1.24    let
    1.25      val (mounted_serializer, prepared_program) = mount_serializer thy
    1.26 -      target NONE "Code" [] naming program deps;
    1.27 -  in evaluation mounted_serializer prepared_program deps end;
    1.28 +      target NONE "Code" [] naming program consts;
    1.29 +  in evaluation mounted_serializer prepared_program consts end;
    1.30  
    1.31  end; (* local *)
    1.32