changeset 59151 | a012574b78e7 |
parent 59150 | 71b416020f42 |
child 59155 | a9a5ddfc2aad |
--- 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");