tuned;
authorwenzelm
Fri Dec 19 20:09:31 2014 +0100 (2014-12-19)
changeset 59153b5e253703ebd
parent 59152 66e6c539a36d
child 59154 68ca25931dce
tuned;
src/HOL/Tools/code_evaluation.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/Tools/code_evaluation.ML	Fri Dec 19 17:23:56 2014 +0100
     1.2 +++ b/src/HOL/Tools/code_evaluation.ML	Fri Dec 19 20:09:31 2014 +0100
     1.3 @@ -174,7 +174,8 @@
     1.4  structure Evaluation = Proof_Data
     1.5  (
     1.6    type T = unit -> term
     1.7 -  fun init _ () = raise Fail "Evaluation"
     1.8 +  val empty: T = fn () => raise Fail "Evaluation"
     1.9 +  fun init _ = empty
    1.10  );
    1.11  val put_term = Evaluation.put;
    1.12  val cookie = (Evaluation.get, put_term, "Code_Evaluation.put_term");
     2.1 --- a/src/Tools/nbe.ML	Fri Dec 19 17:23:56 2014 +0100
     2.2 +++ b/src/Tools/nbe.ML	Fri Dec 19 20:09:31 2014 +0100
     2.3 @@ -233,9 +233,11 @@
     2.4  
     2.5  structure Univs = Proof_Data
     2.6  (
     2.7 -  type T = unit -> Univ list -> Univ list
     2.8 -  fun init _ () = raise Fail "Univs"
     2.9 +  type T = unit -> Univ list -> Univ list;
    2.10 +  val empty: T = fn () => raise Fail "Univs";
    2.11 +  fun init _ = empty;
    2.12  );
    2.13 +val get_result = Univs.get;
    2.14  val put_result = Univs.put;
    2.15  
    2.16  local
    2.17 @@ -247,7 +249,7 @@
    2.18    val name_same = prefix ^ "same";
    2.19  in
    2.20  
    2.21 -val univs_cookie = (Univs.get, put_result, name_put);
    2.22 +val univs_cookie = (get_result, put_result, name_put);
    2.23  
    2.24  fun nbe_fun idx_of 0 (Code_Symbol.Constant "") = "nbe_value"
    2.25    | nbe_fun idx_of i sym = "c_" ^ string_of_int (idx_of sym)