--- a/src/HOL/HOLCF/Cfun.thy Tue Apr 05 13:07:40 2011 +0200
+++ b/src/HOL/HOLCF/Cfun.thy Tue Apr 05 14:25:18 2011 +0200
@@ -56,9 +56,9 @@
(* cf. Syntax.lambda_ast_tr from src/Pure/Syntax/syn_trans.ML *)
let
fun Lambda_ast_tr [pats, body] =
- Syntax.fold_ast_p @{syntax_const "_cabs"}
- (Syntax.unfold_ast @{syntax_const "_cargs"} (Syntax.strip_positions_ast pats), body)
- | Lambda_ast_tr asts = raise Syntax.AST ("Lambda_ast_tr", asts);
+ Ast.fold_ast_p @{syntax_const "_cabs"}
+ (Ast.unfold_ast @{syntax_const "_cargs"} (Syntax.strip_positions_ast pats), body)
+ | Lambda_ast_tr asts = raise Ast.AST ("Lambda_ast_tr", asts);
in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end;
*}
@@ -67,12 +67,12 @@
(* cf. Syntax.abs_ast_tr' from src/Pure/Syntax/syn_trans.ML *)
let
fun cabs_ast_tr' asts =
- (case Syntax.unfold_ast_p @{syntax_const "_cabs"}
- (Syntax.Appl (Syntax.Constant @{syntax_const "_cabs"} :: asts)) of
- ([], _) => raise Syntax.AST ("cabs_ast_tr'", asts)
- | (xs, body) => Syntax.Appl
- [Syntax.Constant @{syntax_const "_Lambda"},
- Syntax.fold_ast @{syntax_const "_cargs"} xs, body]);
+ (case Ast.unfold_ast_p @{syntax_const "_cabs"}
+ (Ast.Appl (Ast.Constant @{syntax_const "_cabs"} :: asts)) of
+ ([], _) => raise Ast.AST ("cabs_ast_tr'", asts)
+ | (xs, body) => Ast.Appl
+ [Ast.Constant @{syntax_const "_Lambda"},
+ Ast.fold_ast @{syntax_const "_cargs"} xs, body]);
in [(@{syntax_const "_cabs"}, cabs_ast_tr')] end
*}