--- a/Nominal/Ex/NoneExamples.thy	Sun Aug 29 12:17:25 2010 +0800
+++ b/Nominal/Ex/NoneExamples.thy	Sun Aug 29 13:36:03 2010 +0800
@@ -1,85 +1,80 @@
 theory NoneExamples
-imports "../NewParser"
+imports "../Nominal2"
 begin
 
+text {*
+  This example is not covered by our binding 
+  specification.
+*}
+
 atom_decl name
 
-
 text {* 
   "Weirdo" example from Peter Sewell's bestiary. 
 
-  This example is not covered by our binding 
-  specification.
-
+  p2 occurs in two bodies
 *}
 
+(*
 nominal_datatype weird =
   Foo_var "name"
 | Foo_pair "weird" "weird" 
 | Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
     bind x in p1 p2, 
     bind y in p2 p3
-
-(* e1 occurs in two bodies *)
+*)
 
-nominal_datatype exp =
-  Var name
-| Pair exp exp
-| LetRec x::name p::pat e1::exp e2::exp  bind x in e1 e2, bind "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"
+text {* 
+  this example binds bound names and therefore the 
+  fv-function is not respectful - the proof just fails.
+*}
 
-
-(* this example binds bound names and
-   so is not respectful *)
 (*
 nominal_datatype trm =
-  Vr "name"
-| Lm x::"name" t::"trm"         bind x in t
-| Lt left::"trm" right::"trm"   bind "bv left" in right
+  Var "name"
+| Lam x::"name" t::"trm"         bind x in t
+| Let left::"trm" right::"trm"   bind (set) "bv left" in right
 binder
   bv
 where
-  "bv (Vr n) = {}"
-| "bv (Lm n t) = {atom n} \<union> bv t"
-| "bv (Lt l r) = bv l \<union> bv r"
+  "bv (Var n) = {}"
+| "bv (Lam n t) = {atom n} \<union> bv t"
+| "bv (Let l r) = bv l \<union> bv r"
 *)
 
-(* this example uses "-" in the binding function; 
-   at the moment this is unsupported *)
+text {* 
+  this example uses "-" in the binding function; 
+  at the moment this is unsupported 
+*}
+
 (*
 nominal_datatype trm' =
-  Vr' "name"
-| Lm' l::"name" r::"trm'"   bind l in r
-| Lt' l::"trm'" r::"trm'"   bind "bv' l" in r
+  Var "name"
+| Lam l::"name" r::"trm'"   bind l in r
+| Let l::"trm'" r::"trm'"   bind (set) "bv' l" in r
 binder
   bv'
 where
-  "bv' (Vr' n) = {atom n}"
-| "bv' (Lm' n t) = bv' t - {atom n}"
-| "bv' (Lt' l r) = bv' l \<union> bv' r"
+  "bv' (Var n) = {atom n}"
+| "bv' (Lam n t) = bv' t - {atom n}"
+| "bv' (Let l r) = bv' l \<union> bv' r"
 *)
 
-(* this example again binds bound names  *)
+text {* 
+  again this example binds bound names - so not respectful
+*}
+
 (*
-nominal_datatype trm'' =
-  Va'' "name"
-| Lm'' n::"name" l::"trm''" bind n in l
-and bla'' =
-  Bla'' f::"trm''" s::"trm''" bind "bv'' f" in s
+nominal_datatype trm =
+  Var "name"
+| Lam n::"name" l::"trm" bind n in l
+and bla =
+  Bla f::"trm" s::"trm" bind (set) "bv f" in s
 binder
-  bv''
+  bv :: "trm \<Rightarrow> atom set"
 where
-  "bv'' (Vm'' x) = {}"
-| "bv'' (Lm'' x b) = {atom x}"
+  "bv (Vam x) = {}"
+| "bv (Lam x b) = {atom x}"
 *)
 
 end