--- a/Nominal/Test.thy	Mon Mar 01 11:40:48 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 01 14:26:14 2010 +0100
@@ -7,9 +7,9 @@
 nominal_datatype lam =
   VAR "name"
 | APP "lam" "lam"
-| LET bp::"bp" t::"lam"   bind "bi bp" in t ("Let _ in _" [100,100] 100)
+| LET bp::"bp" t::"lam"   bind "bi bp" in t
 and bp = 
-  BP "name" "lam"  ("_ ::= _" [100,100] 100)
+  BP "name" "lam" 
 binder
   bi::"bp \<Rightarrow> name set"
 where