src/HOL/Tools/code_evaluation.ML
changeset 41184 5c6f44d22f51
parent 40726 16dcfedc4eb7
child 41247 c5cb19ecbd41
     1.1 --- a/src/HOL/Tools/code_evaluation.ML	Tue Dec 14 00:16:30 2010 +0100
     1.2 +++ b/src/HOL/Tools/code_evaluation.ML	Wed Dec 15 09:47:12 2010 +0100
     1.3 @@ -12,8 +12,8 @@
     1.4    val static_value: theory -> string list -> typ list -> term -> term option
     1.5    val static_value_strict: theory -> string list -> typ list -> term -> term
     1.6    val static_value_exn: theory -> string list -> typ list -> term -> term Exn.result
     1.7 -  val dynamic_eval_conv: conv
     1.8 -  val static_eval_conv: theory -> string list -> typ list -> conv
     1.9 +  val dynamic_conv: conv
    1.10 +  val static_conv: theory -> string list -> typ list -> conv
    1.11    val put_term: (unit -> term) -> Proof.context -> Proof.context
    1.12    val tracing: string -> 'a -> 'a
    1.13    val setup: theory -> theory
    1.14 @@ -194,10 +194,10 @@
    1.15            error ("Failed to certify evaluation result of " ^ Syntax.string_of_term_global thy t)
    1.16    end;
    1.17  
    1.18 -val dynamic_eval_conv = Conv.tap_thy
    1.19 +val dynamic_conv = Conv.tap_thy
    1.20    (fn thy => certify_eval thy (dynamic_value thy) Code_Runtime.dynamic_holds_conv);
    1.21  
    1.22 -fun static_eval_conv thy consts Ts =
    1.23 +fun static_conv thy consts Ts =
    1.24    let
    1.25      val eqs = "==" :: @{const_name HOL.eq} ::
    1.26        map (fn T => AxClass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts;