Nominal/Ex/CPS/Lt.thy
changeset 3089 9bcf02a6eea9
parent 2998 f0fab367453a
child 3186 425b4c406d80
--- 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 \<Rightarrow> name \<Rightarrow> lt \<Rightarrow> lt"  ("_ [_ ::= _]" [90, 90, 90] 90)