src/HOL/HOL.thy
changeset 52143 36ffe23b25f8
parent 51798 ad3a241def73
child 52230 1105b3b5aa77
     1.1 --- a/src/HOL/HOL.thy	Sat May 25 15:00:53 2013 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat May 25 15:37:53 2013 +0200
     1.3 @@ -116,7 +116,7 @@
     1.4  syntax "_The" :: "[pttrn, bool] => 'a"  ("(3THE _./ _)" [0, 10] 10)
     1.5  translations "THE x. P" == "CONST The (%x. P)"
     1.6  print_translation {*
     1.7 -  [(@{const_syntax The}, fn [Abs abs] =>
     1.8 +  [(@{const_syntax The}, fn _ => fn [Abs abs] =>
     1.9        let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
    1.10        in Syntax.const @{syntax_const "_The"} $ x $ t end)]
    1.11  *}  -- {* To avoid eta-contraction of body *}