src/HOL/Code_Evaluation.thy
changeset 39471 55e0ff582fa4
parent 39403 aad9f3cfa1d9
child 39564 acfd10e38e80
--- a/src/HOL/Code_Evaluation.thy	Thu Sep 16 08:18:34 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy	Thu Sep 16 16:51:33 2010 +0200
@@ -315,8 +315,8 @@
 
 fun tracing s x = (Output.tracing s; x);
 
-fun eval_term thy t = Code_Runtime.value NONE (Evaluation.get, put_term, "Code_Evaluation.put_term")
-  I thy (HOLogic.mk_term_of (fastype_of t) t) [];
+fun eval_term thy t = Code_Runtime.dynamic_value_strict (Evaluation.get, put_term, "Code_Evaluation.put_term")
+  thy NONE I (HOLogic.mk_term_of (fastype_of t) t) [];
 
 end
 *}