| changeset 42284 | 326f57825e1a |
| parent 40703 | d1fc454d6735 |
| child 44890 | 22f665a2e91c |
--- a/src/HOL/Hilbert_Choice.thy Fri Apr 08 11:39:45 2011 +0200 +++ b/src/HOL/Hilbert_Choice.thy Fri Apr 08 13:31:16 2011 +0200 @@ -26,7 +26,7 @@ print_translation {* [(@{const_syntax Eps}, fn [Abs abs] => - let val (x, t) = atomic_abs_tr' abs + let val (x, t) = Syntax_Trans.atomic_abs_tr' abs in Syntax.const @{syntax_const "_Eps"} $ x $ t end)] *} -- {* to avoid eta-contraction of body *}