src/HOL/Hilbert_Choice.thy
changeset 42284 326f57825e1a
parent 40703 d1fc454d6735
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Fri Apr 08 11:39:45 2011 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Fri Apr 08 13:31:16 2011 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  
     1.5  print_translation {*
     1.6    [(@{const_syntax Eps}, 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 "_Eps"} $ x $ t end)]
    1.10  *} -- {* to avoid eta-contraction of body *}
    1.11