src/Tools/Code/code_target.ML
changeset 63157 65a81a4ef7f8
parent 63024 adeac19dd410
child 63159 84c6dd947b75
     1.1 --- a/src/Tools/Code/code_target.ML	Thu May 26 15:27:50 2016 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Thu May 26 15:27:50 2016 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4      -> ((string * bool) * Token.T list) list -> unit
     1.5  
     1.6    val generatedN: string
     1.7 -  val evaluator: Proof.context -> string -> Code_Thingol.program
     1.8 +  val computation_text: Proof.context -> string -> Code_Thingol.program
     1.9      -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
    1.10      -> (string * string) list * string
    1.11  
    1.12 @@ -396,7 +396,7 @@
    1.13      else Isabelle_System.with_tmp_dir "Code_Test" ext_check
    1.14    end;
    1.15  
    1.16 -fun subevaluator mounted_serializer prepared_program syms all_public ((vs, ty), t) =
    1.17 +fun dynamic_computation_text mounted_serializer prepared_program syms all_public ((vs, ty), t) =
    1.18    let
    1.19      val _ = if Code_Thingol.contains_dict_var t then
    1.20        error "Term to be evaluated contains free dictionaries" else ();
    1.21 @@ -413,11 +413,11 @@
    1.22      val value_name = the (deresolve Code_Symbol.value);
    1.23    in (program_code, value_name) end;
    1.24  
    1.25 -fun evaluator ctxt target_name program syms =
    1.26 +fun computation_text ctxt target_name program syms =
    1.27    let
    1.28      val (mounted_serializer, (_, prepared_program)) =
    1.29        mount_serializer ctxt target_name NONE generatedN [] program syms;
    1.30 -  in subevaluator mounted_serializer prepared_program syms end;
    1.31 +  in dynamic_computation_text mounted_serializer prepared_program syms end;
    1.32  
    1.33  end; (* local *)
    1.34