diff -r 87894b5156f4 -r 8557af71724e Nominal/Test.thy --- 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 \ name set" where