changeset 42284 | 326f57825e1a |
parent 42178 | b992c8e6394b |
child 42361 | 23f352990944 |
--- a/src/HOL/HOL.thy Fri Apr 08 11:39:45 2011 +0200 +++ b/src/HOL/HOL.thy Fri Apr 08 13:31:16 2011 +0200 @@ -130,7 +130,7 @@ print_translation {* [(@{const_syntax The}, 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 "_The"} $ x $ t end)] *} -- {* To avoid eta-contraction of body *}