changeset 59151 | a012574b78e7 |
parent 59058 | a78612c67ec0 |
child 59153 | b5e253703ebd |
--- a/src/HOL/Tools/code_evaluation.ML Fri Dec 19 12:36:50 2014 +0100 +++ b/src/HOL/Tools/code_evaluation.ML Fri Dec 19 12:56:06 2014 +0100 @@ -174,8 +174,7 @@ structure Evaluation = Proof_Data ( type T = unit -> term - (* FIXME avoid user error with non-user text *) - fun init _ () = error "Evaluation" + fun init _ () = raise Fail "Evaluation" ); val put_term = Evaluation.put; val cookie = (Evaluation.get, put_term, "Code_Evaluation.put_term");