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