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