tuned;

--- a/src/Tools/Code/code_runtime.ML	Fri Dec 19 20:10:59 2014 +0100
+++ b/src/Tools/Code/code_runtime.ML	Fri Dec 19 20:32:54 2014 +0100
@@ -159,8 +159,9 @@
 
 structure Truth_Result = Proof_Data
 (
-  type T = unit -> truth
-  fun init _ () = raise Fail "Truth_Result"
+  type T = unit -> truth;
+  val empty: T = fn () => raise Fail "Truth_Result";
+  fun init _ = empty;
 );
 val put_truth = Truth_Result.put;
 val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth");