--- a/src/HOL/HOLCF/Cfun.thy Tue Mar 22 18:03:28 2011 +0100
+++ b/src/HOL/HOLCF/Cfun.thy Tue Mar 22 20:44:47 2011 +0100
@@ -30,8 +30,6 @@
subsection {* Syntax for continuous lambda abstraction *}
-declare [[syntax_positions = false]] (* FIXME pattern translations choke on position constraints *)
-
syntax "_cabs" :: "[logic, logic] \<Rightarrow> logic"
parse_translation {*
@@ -59,7 +57,7 @@
let
fun Lambda_ast_tr [pats, body] =
Syntax.fold_ast_p @{syntax_const "_cabs"}
- (Syntax.unfold_ast @{syntax_const "_cargs"} pats, body)
+ (Syntax.unfold_ast @{syntax_const "_cargs"} (Syntax.strip_positions_ast pats), body)
| Lambda_ast_tr asts = raise Syntax.AST ("Lambda_ast_tr", asts);
in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end;
*}