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