1.1 --- a/src/HOL/HOLCF/Cfun.thy	Tue Apr 05 13:07:40 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Tue Apr 05 14:25:18 2011 +0200
     1.3 @@ -56,9 +56,9 @@
     1.4  (* cf. Syntax.lambda_ast_tr from src/Pure/Syntax/syn_trans.ML *)
     1.5    let
     1.6      fun Lambda_ast_tr [pats, body] =
     1.7 -          Syntax.fold_ast_p @{syntax_const "_cabs"}
     1.8 -            (Syntax.unfold_ast @{syntax_const "_cargs"} (Syntax.strip_positions_ast pats), body)
     1.9 -      | Lambda_ast_tr asts = raise Syntax.AST ("Lambda_ast_tr", asts);
    1.10 +          Ast.fold_ast_p @{syntax_const "_cabs"}
    1.11 +            (Ast.unfold_ast @{syntax_const "_cargs"} (Syntax.strip_positions_ast pats), body)
    1.12 +      | Lambda_ast_tr asts = raise Ast.AST ("Lambda_ast_tr", asts);
    1.13    in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end;
    1.14  *}
    1.15  
    1.16 @@ -67,12 +67,12 @@
    1.17  (* cf. Syntax.abs_ast_tr' from src/Pure/Syntax/syn_trans.ML *)
    1.18    let
    1.19      fun cabs_ast_tr' asts =
    1.20 -      (case Syntax.unfold_ast_p @{syntax_const "_cabs"}
    1.21 -          (Syntax.Appl (Syntax.Constant @{syntax_const "_cabs"} :: asts)) of
    1.22 -        ([], _) => raise Syntax.AST ("cabs_ast_tr'", asts)
    1.23 -      | (xs, body) => Syntax.Appl
    1.24 -          [Syntax.Constant @{syntax_const "_Lambda"},
    1.25 -           Syntax.fold_ast @{syntax_const "_cargs"} xs, body]);
    1.26 +      (case Ast.unfold_ast_p @{syntax_const "_cabs"}
    1.27 +          (Ast.Appl (Ast.Constant @{syntax_const "_cabs"} :: asts)) of
    1.28 +        ([], _) => raise Ast.AST ("cabs_ast_tr'", asts)
    1.29 +      | (xs, body) => Ast.Appl
    1.30 +          [Ast.Constant @{syntax_const "_Lambda"},
    1.31 +           Ast.fold_ast @{syntax_const "_cargs"} xs, body]);
    1.32    in [(@{syntax_const "_cabs"}, cabs_ast_tr')] end
    1.33  *}
    1.34