src/HOL/HOLCF/Cfun.thy
changeset 52143 36ffe23b25f8
parent 51717 9e7d1c139569
child 57945 cacb00a569e0
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Sat May 25 15:00:53 2013 +0200
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Sat May 25 15:37:53 2013 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4  *}
     1.5  
     1.6  print_translation {*
     1.7 -  [(@{const_syntax Abs_cfun}, fn [Abs abs] =>
     1.8 +  [(@{const_syntax Abs_cfun}, fn _ => fn [Abs abs] =>
     1.9        let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
    1.10        in Syntax.const @{syntax_const "_cabs"} $ x $ t end)]
    1.11  *}  -- {* To avoid eta-contraction of body *}
    1.12 @@ -61,7 +61,7 @@
    1.13            Ast.fold_ast_p @{syntax_const "_cabs"}
    1.14              (Ast.unfold_ast @{syntax_const "_cargs"} (Ast.strip_positions pats), body)
    1.15        | Lambda_ast_tr asts = raise Ast.AST ("Lambda_ast_tr", asts);
    1.16 -  in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end;
    1.17 +  in [(@{syntax_const "_Lambda"}, K Lambda_ast_tr)] end;
    1.18  *}
    1.19  
    1.20  print_ast_translation {*
    1.21 @@ -75,7 +75,7 @@
    1.22        | (xs, body) => Ast.Appl
    1.23            [Ast.Constant @{syntax_const "_Lambda"},
    1.24             Ast.fold_ast @{syntax_const "_cargs"} xs, body]);
    1.25 -  in [(@{syntax_const "_cabs"}, cabs_ast_tr')] end
    1.26 +  in [(@{syntax_const "_cabs"}, K cabs_ast_tr')] end
    1.27  *}
    1.28  
    1.29  text {* Dummy patterns for continuous abstraction *}