src/Tools/Code/code_runtime.ML
changeset 59151 a012574b78e7
parent 59150 71b416020f42
child 59155 a9a5ddfc2aad
     1.1 --- a/src/Tools/Code/code_runtime.ML	Fri Dec 19 12:36:50 2014 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Dec 19 12:56:06 2014 +0100
     1.3 @@ -160,8 +160,7 @@
     1.4  structure Truth_Result = Proof_Data
     1.5  (
     1.6    type T = unit -> truth
     1.7 -  (* FIXME avoid user error with non-user text *)
     1.8 -  fun init _ () = error "Truth_Result"
     1.9 +  fun init _ () = raise Fail "Truth_Result"
    1.10  );
    1.11  val put_truth = Truth_Result.put;
    1.12  val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth");