diff -r 71b416020f42 -r a012574b78e7 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Fri Dec 19 12:36:50 2014 +0100
+++ b/src/Tools/Code/code_runtime.ML	Fri Dec 19 12:56:06 2014 +0100
@@ -160,8 +160,7 @@
 structure Truth_Result = Proof_Data
 (
   type T = unit -> truth
-  (* FIXME avoid user error with non-user text *)
-  fun init _ () = error "Truth_Result"
+  fun init _ () = raise Fail "Truth_Result"
 );
 val put_truth = Truth_Result.put;
 val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth");