src/HOL/HOL.thy
changeset 42284 326f57825e1a
parent 42178 b992c8e6394b
child 42361 23f352990944
     1.1 --- a/src/HOL/HOL.thy	Fri Apr 08 11:39:45 2011 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Apr 08 13:31:16 2011 +0200
     1.3 @@ -130,7 +130,7 @@
     1.4  
     1.5  print_translation {*
     1.6    [(@{const_syntax The}, fn [Abs abs] =>
     1.7 -      let val (x, t) = atomic_abs_tr' abs
     1.8 +      let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
     1.9        in Syntax.const @{syntax_const "_The"} $ x $ t end)]
    1.10  *}  -- {* To avoid eta-contraction of body *}
    1.11