| changeset 30947 | dd551284a300 |
| parent 30427 | dfd31c1db060 |
| child 30970 | 3fe2e418a071 |
--- a/src/HOL/Code_Eval.thy Fri Apr 17 14:29:55 2009 +0200 +++ b/src/HOL/Code_Eval.thy Fri Apr 17 14:29:56 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; *}