src/HOL/Code_Evaluation.thy
changeset 34028 1e6206763036
parent 33632 6ea8a4cce9e7
child 35299 4f4d5bf4ea08
     1.1 --- a/src/HOL/Code_Evaluation.thy	Mon Dec 07 14:54:28 2009 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Mon Dec 07 16:27:48 2009 +0100
     1.3 @@ -279,7 +279,7 @@
     1.4  val eval_ref = Unsynchronized.ref (NONE : (unit -> term) option);
     1.5  
     1.6  fun eval_term thy t =
     1.7 -  Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
     1.8 +  Code_Eval.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
     1.9  
    1.10  end;
    1.11  *}