src/HOL/Hilbert_Choice.thy
changeset 52143 36ffe23b25f8
parent 50105 65d5b18e1626
child 54295 45a5523d4a63
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Sat May 25 15:00:53 2013 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Sat May 25 15:37:53 2013 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4    "SOME x. P" == "CONST Eps (%x. P)"
     1.5  
     1.6  print_translation {*
     1.7 -  [(@{const_syntax Eps}, fn [Abs abs] =>
     1.8 +  [(@{const_syntax Eps}, fn _ => fn [Abs abs] =>
     1.9        let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
    1.10        in Syntax.const @{syntax_const "_Eps"} $ x $ t end)]
    1.11  *} -- {* to avoid eta-contraction of body *}