--- a/src/HOL/Code_Evaluation.thy Tue Sep 29 14:59:24 2009 +0200
+++ b/src/HOL/Code_Evaluation.thy Tue Sep 29 16:24:36 2009 +0200
@@ -249,14 +249,14 @@
ML {*
signature EVAL =
sig
- val eval_ref: (unit -> term) option ref
+ val eval_ref: (unit -> term) option Unsynchronized.ref
val eval_term: theory -> term -> term
end;
structure Eval : EVAL =
struct
-val eval_ref = ref (NONE : (unit -> term) option);
+val eval_ref = Unsynchronized.ref (NONE : (unit -> term) option);
fun eval_term thy t =
Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];