src/Tools/Code/code_runtime.ML
changeset 59155 a9a5ddfc2aad
parent 59151 a012574b78e7
child 59621 291934bac95e
     1.1 --- a/src/Tools/Code/code_runtime.ML	Fri Dec 19 20:10:59 2014 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Dec 19 20:32:54 2014 +0100
     1.3 @@ -159,8 +159,9 @@
     1.4  
     1.5  structure Truth_Result = Proof_Data
     1.6  (
     1.7 -  type T = unit -> truth
     1.8 -  fun init _ () = raise Fail "Truth_Result"
     1.9 +  type T = unit -> truth;
    1.10 +  val empty: T = fn () => raise Fail "Truth_Result";
    1.11 +  fun init _ = empty;
    1.12  );
    1.13  val put_truth = Truth_Result.put;
    1.14  val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth");