src/HOL/Code_Evaluation.thy
changeset 39401 887f4218a39a
parent 39387 6608c4838ff9
child 39403 aad9f3cfa1d9
--- a/src/HOL/Code_Evaluation.thy	Wed Sep 15 15:11:40 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy	Wed Sep 15 15:31:32 2010 +0200
@@ -315,7 +315,7 @@
 
 fun tracing s x = (Output.tracing s; x);
 
-fun eval_term thy t = Code_Eval.eval NONE (Evaluation.get, put_term, "Code_Evaluation.put_term")
+fun eval_term thy t = Code_Runtime.eval NONE (Evaluation.get, put_term, "Code_Evaluation.put_term")
   I thy (HOLogic.mk_term_of (fastype_of t) t) [];
 
 end