tuned;

--- a/src/HOL/Tools/code_evaluation.ML	Fri Dec 19 17:23:56 2014 +0100
+++ b/src/HOL/Tools/code_evaluation.ML	Fri Dec 19 20:09:31 2014 +0100
@@ -174,7 +174,8 @@
 structure Evaluation = Proof_Data
 (
   type T = unit -> term
-  fun init _ () = raise Fail "Evaluation"
+  val empty: T = fn () => raise Fail "Evaluation"
+  fun init _ = empty
 );
 val put_term = Evaluation.put;
 val cookie = (Evaluation.get, put_term, "Code_Evaluation.put_term");

--- a/src/Tools/nbe.ML	Fri Dec 19 17:23:56 2014 +0100
+++ b/src/Tools/nbe.ML	Fri Dec 19 20:09:31 2014 +0100
@@ -233,9 +233,11 @@
 
 structure Univs = Proof_Data
 (
-  type T = unit -> Univ list -> Univ list
-  fun init _ () = raise Fail "Univs"
+  type T = unit -> Univ list -> Univ list;
+  val empty: T = fn () => raise Fail "Univs";
+  fun init _ = empty;
 );
+val get_result = Univs.get;
 val put_result = Univs.put;
 
 local
@@ -247,7 +249,7 @@
   val name_same = prefix ^ "same";
 in
 
-val univs_cookie = (Univs.get, put_result, name_put);
+val univs_cookie = (get_result, put_result, name_put);
 
 fun nbe_fun idx_of 0 (Code_Symbol.Constant "") = "nbe_value"
   | nbe_fun idx_of i sym = "c_" ^ string_of_int (idx_of sym)