src/HOL/HOLCF/Cfun.thy
changeset 41478 18500bd1f47b
parent 41430 1aa23e9f2c87
child 41479 655f583840d0
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Sat Jan 08 09:34:08 2011 -0800
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Sat Jan 08 10:02:43 2011 -0800
     1.3 @@ -37,21 +37,11 @@
     1.4    [mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_cfun})];
     1.5  *}
     1.6  
     1.7 -text {* To avoid eta-contraction of body: *}
     1.8 -typed_print_translation {*
     1.9 -  let
    1.10 -    fun cabs_tr' _ _ [Abs abs] = let
    1.11 -          val (x,t) = atomic_abs_tr' abs
    1.12 -        in Syntax.const @{syntax_const "_cabs"} $ x $ t end
    1.13 -
    1.14 -      | cabs_tr' _ T [t] = let
    1.15 -          val xT = domain_type (domain_type T);
    1.16 -          val abs' = ("x",xT,(incr_boundvars 1 t)$Bound 0);
    1.17 -          val (x,t') = atomic_abs_tr' abs';
    1.18 -        in Syntax.const @{syntax_const "_cabs"} $ x $ t' end;
    1.19 -
    1.20 -  in [(@{const_syntax Abs_cfun}, cabs_tr')] end;
    1.21 -*}
    1.22 +print_translation {*
    1.23 +  [(@{const_syntax Abs_cfun}, fn [Abs abs] =>
    1.24 +      let val (x, t) = atomic_abs_tr' abs
    1.25 +      in Syntax.const @{syntax_const "_cabs"} $ x $ t end)]
    1.26 +*}  -- {* To avoid eta-contraction of body *}
    1.27  
    1.28  text {* Syntax for nested abstractions *}
    1.29