src/HOL/HOLCF/Cfun.thy
changeset 42057 3eba96ff3d3e
parent 42056 160a630b2c7e
child 42151 4da4fc77664b
--- 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;
 *}