--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/LetFun.thy	Sun Aug 29 13:36:03 2010 +0800
@@ -0,0 +1,25 @@
+theory LetFun
+imports "../Nominal2"
+begin
+
+atom_decl name
+
+(* x is bound in both e1 and e2
+   names in p are bound only in e1 *)
+
+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
+and pat =
+  PVar name
+| PUnit
+| PPair pat pat
+binder
+  bp :: "pat \<Rightarrow> atom list"
+where
+  "bp (PVar x) = [atom x]"
+| "bp (PUnit) = []"
+| "bp (PPair p1 p2) = bp p1 @ bp p2"
+
+end
\ No newline at end of file