Nominal/Ex/LetFun.thy
changeset 2950 0911cb7bf696
parent 2616 dd7490fdd998
child 3029 6fd3fc3254ee
--- a/Nominal/Ex/LetFun.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/LetFun.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -12,7 +12,7 @@
 nominal_datatype exp =
   Var name
 | Pair exp exp
-| LetRec x::name p::pat e1::exp e2::exp  bind x in e2, bind x "bp p" in e1
+| LetRec x::name p::pat e1::exp e2::exp  binds x in e2, binds x "bp p" in e1
 and pat =
   PVar name
 | PUnit