src/HOL/Tools/code_evaluation.ML

 (** evaluation **)
 
 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");
 
 fun mk_term_of t = HOLogic.mk_term_of (fastype_of t) t;