# HG changeset patch
# User huffman
# Date 1200684868 -3600
# Node ID 9c544dac6269e9a687210efa869e0706a58acdd2
# Parent  aa0eca1ccb19bcd20950689db41e76af06f355f3
add space to binder syntax

diff -r aa0eca1ccb19 -r 9c544dac6269 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Fri Jan 18 20:31:11 2008 +0100
+++ b/src/HOLCF/Cfun.thy	Fri Jan 18 20:34:28 2008 +0100
@@ -68,7 +68,7 @@
   "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic"  ("(3LAM _./ _)" [1000, 10] 10)
 
 syntax (xsymbols)
-  "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic" ("(3\<Lambda>_./ _)" [1000, 10] 10)
+  "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic" ("(3\<Lambda> _./ _)" [1000, 10] 10)
 
 parse_ast_translation {*
 (* rewrites (LAM x y z. t) => (_cabs x (_cabs y (_cabs z t))) *)
diff -r aa0eca1ccb19 -r 9c544dac6269 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Fri Jan 18 20:31:11 2008 +0100
+++ b/src/HOLCF/Fix.thy	Fri Jan 18 20:34:28 2008 +0100
@@ -59,7 +59,7 @@
   "_FIX" :: "['a, 'a] \<Rightarrow> 'a" ("(3FIX _./ _)" [1000, 10] 10)
 
 syntax (xsymbols)
-  "_FIX" :: "['a, 'a] \<Rightarrow> 'a" ("(3\<mu>_./ _)" [1000, 10] 10)
+  "_FIX" :: "['a, 'a] \<Rightarrow> 'a" ("(3\<mu> _./ _)" [1000, 10] 10)
 
 translations
   "\<mu> x. t" == "CONST fix\<cdot>(\<Lambda> x. t)"