| changeset 30957 | 20d01210b9b1 |
| parent 30947 | dd551284a300 |
| child 30970 | 3fe2e418a071 |
--- a/src/HOL/Code_Eval.thy Mon Apr 20 12:27:23 2009 +0200 +++ b/src/HOL/Code_Eval.thy Mon Apr 20 16:28:13 2009 +0200 @@ -175,8 +175,7 @@ fun eval_term thy t = t |> Eval.mk_term_of (fastype_of t) - |> (fn t => Code_ML.eval_term ("Eval.eval_ref", eval_ref) thy t []) - |> Code.postprocess_term thy; + |> (fn t => Code_ML.eval_term NONE ("Eval.eval_ref", eval_ref) thy t []); end; *}