src/HOL/Code_Evaluation.thy
changeset 39403 aad9f3cfa1d9
parent 39401 887f4218a39a
child 39471 55e0ff582fa4
--- a/src/HOL/Code_Evaluation.thy	Wed Sep 15 15:35:01 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy	Wed Sep 15 15:40:35 2010 +0200
@@ -315,7 +315,7 @@
 
 fun tracing s x = (Output.tracing s; x);
 
-fun eval_term thy t = Code_Runtime.eval NONE (Evaluation.get, put_term, "Code_Evaluation.put_term")
+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) [];
 
 end