diff -r 5e74bd87bcda -r 9bcf02a6eea9 Nominal/Ex/CPS/Lt.thy --- a/Nominal/Ex/CPS/Lt.thy Wed Dec 21 15:47:42 2011 +0900 +++ b/Nominal/Ex/CPS/Lt.thy Wed Dec 21 17:05:00 2011 +0900 @@ -7,8 +7,8 @@ nominal_datatype lt = Var name ("_~" [150] 149) + | App lt lt (infixl "$" 100) | Lam x::"name" t::"lt" binds x in t - | App lt lt (infixl "$" 100) nominal_primrec subst :: "lt \ name \ lt \ lt" ("_ [_ ::= _]" [90, 90, 90] 90)