src/HOL/Tools/code_evaluation.ML

--- 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");