--- a/Nominal/Abs.thy	Wed Mar 17 09:17:55 2010 +0100
+++ b/Nominal/Abs.thy	Wed Mar 17 09:18:27 2010 +0100
@@ -2,11 +2,27 @@
 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product"
 begin
 
+lemma permute_boolI:
+  fixes P::"bool"
+  shows "p \<bullet> P \<Longrightarrow> P"
+apply(simp add: permute_bool_def)
+done
+
+lemma permute_boolE:
+  fixes P::"bool"
+  shows "P \<Longrightarrow> p \<bullet> P"
+apply(simp add: permute_bool_def)
+done
+
 fun
   alpha_gen 
 where
   alpha_gen[simp del]:
-  "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow> f x - bs = f y - cs \<and> (f x - bs) \<sharp>* pi \<and> R (pi \<bullet> x) y"
+  "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow> 
+     f x - bs = f y - cs \<and> 
+     (f x - bs) \<sharp>* pi \<and> 
+     R (pi \<bullet> x) y \<and>
+     pi \<bullet> bs = cs"
 
 notation
   alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100)
@@ -23,7 +39,11 @@
   assumes a: "(bs, x) \<approx>gen R f p (cs, y)"
   and     b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
   shows "(cs, y) \<approx>gen R f (- p) (bs, x)"
-  using a b by (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm)
+  using a b 
+  apply (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm)
+  apply(clarify)
+  apply(simp)
+  done
 
 lemma alpha_gen_trans:
   assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)"
@@ -60,6 +80,8 @@
   apply(simp add: fresh_star_def fresh_minus_perm)
   apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
   apply simp
+  apply(clarify)
+  apply(simp)
   apply(rule a)
   apply assumption
   done
@@ -76,10 +98,10 @@
   apply(simp add: fresh_star_plus)
   apply(drule_tac x="- pia \<bullet> sa" in spec)
   apply(drule mp)
-  apply(rotate_tac 4)
+  apply(rotate_tac 5)
   apply(drule_tac pi="- pia" in a)
   apply(simp)
-  apply(rotate_tac 6)
+  apply(rotate_tac 7)
   apply(drule_tac pi="pia" in a)
   apply(simp)
   done
@@ -102,7 +124,7 @@
   apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
   apply(subst permute_eqvt[symmetric])
   apply(simp)
-  done
+  sorry
 
 fun
   alpha_abs 
@@ -112,6 +134,8 @@
 notation
   alpha_abs ("_ \<approx>abs _")
 
+
+
 lemma alpha_abs_swap:
   assumes a1: "a \<notin> (supp x) - bs"
   and     a2: "b \<notin> (supp x) - bs"
@@ -346,23 +370,6 @@
 notation 
   alpha2 ("_ \<approx>abs2 _")
 
-lemma qq:
-  fixes S::"atom set"
-  assumes a: "supp p \<inter> S = {}"
-  shows "p \<bullet> S = S"
-using a
-apply(simp add: supp_perm permute_set_eq)
-apply(auto)
-apply(simp only: disjoint_iff_not_equal)
-apply(simp)
-apply (metis permute_atom_def_raw)
-apply(rule_tac x="(- p) \<bullet> x" in exI)
-apply(simp)
-apply(simp only: disjoint_iff_not_equal)
-apply(simp)
-apply(metis permute_minus_cancel)
-done
-
 lemma alpha_old_new:
   assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b"
   shows "({a}, x) \<approx>abs ({b}, y)"
@@ -385,6 +392,7 @@
 apply(simp)
 apply(simp)
 apply(simp add: permute_set_eq)
+apply(rule conjI)
 apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1])
 apply(simp add: permute_self)
 apply(simp add: Diff_eqvt supp_eqvt)
@@ -393,6 +401,7 @@
 apply(simp add: fresh_star_def fresh_def)
 apply(blast)
 apply(simp add: supp_swap)
+apply(simp add: eqvts)
 done
 
 lemma perm_zero:
@@ -532,9 +541,42 @@
 apply(simp add: zero)
 apply(rotate_tac 3)
 oops
-lemma tt:
-  "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"
-oops
+
+lemma ii:
+  assumes "\<forall>x \<in> A. p \<bullet> x = x"
+  shows "p \<bullet> A = A"
+using assms
+apply(auto)
+apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_bound inf_Int_eq mem_def mem_permute_iff)
+apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_apply eqvt_bound eqvt_lambda inf_Int_eq mem_def mem_permute_iff permute_minus_cancel(2) permute_pure)
+done
+
+
+
+lemma alpha_abs_Pair:
+  shows "(bs, (x1, x2)) \<approx>gen (\<lambda>(x1,x2) (y1,y2). x1=y1 \<and> x2=y2) (\<lambda>(x,y). supp x \<union> supp y) p (cs, (y1, y2))
+         \<longleftrightarrow> ((bs, x1) \<approx>gen (op=) supp p (cs, y1) \<and> (bs, x2) \<approx>gen (op=) supp p (cs, y2))"         
+  apply(simp add: alpha_gen)
+  apply(simp add: fresh_star_def)
+  apply(simp add: ball_Un Un_Diff)
+  apply(rule iffI)
+  apply(simp)
+  defer
+  apply(simp)
+  apply(rule conjI)
+  apply(clarify)
+  apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
+  apply(rule sym)
+  apply(rule ii)
+  apply(simp add: fresh_def supp_perm)
+  apply(clarify)
+  apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
+  apply(simp add: fresh_def supp_perm)
+  apply(rule sym)
+  apply(rule ii)
+  apply(simp)
+  done
+
 
 lemma yy:
   assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2"
@@ -543,18 +585,6 @@
 apply (metis insert_Diff_single insert_absorb)
 done
 
-lemma permute_boolI:
-  fixes P::"bool"
-  shows "p \<bullet> P \<Longrightarrow> P"
-apply(simp add: permute_bool_def)
-done
-
-lemma permute_boolE:
-  fixes P::"bool"
-  shows "P \<Longrightarrow> p \<bullet> P"
-apply(simp add: permute_bool_def)
-done
-
 lemma kk:
   assumes a: "p \<bullet> x = y"
   shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y"

--- a/Nominal/Test.thy	Wed Mar 17 09:17:55 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 17 09:18:27 2010 +0100
@@ -74,19 +74,6 @@
 apply(simp only: eqvts)
 apply(simp only: supp_Abs)
 (* LET case *)
-defer
-(* BP case *)
-apply(simp only: supp_def)
-apply(simp only: lam_bp_perm)
-apply(simp only: lam_bp_inject)
-apply(simp only: de_Morgan_conj)
-apply(simp only: Collect_disj_eq)
-apply(simp only: infinite_Un)
-apply(simp only: Collect_disj_eq)
-apply(simp only: supp_def[symmetric])
-apply(simp only: supp_at_base)
-apply(simp)
-(* LET case *)
 apply(rule_tac t="supp (LET bp_raw lam_raw)" and s="supp (Abs (bi bp_raw) lam_raw) \<union> fv_bi bp_raw" in subst)
 apply(simp (no_asm) only: supp_def)
 apply(simp only: lam_bp_perm)
@@ -105,12 +92,110 @@
 apply(blast)
 apply(simp add: supp_Abs)
 apply(blast)
+(* BP case *)
+apply(simp only: supp_def)
+apply(simp only: lam_bp_perm)
+apply(simp only: lam_bp_inject)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: infinite_Un)
+apply(simp only: Collect_disj_eq)
+apply(simp only: supp_def[symmetric])
+apply(simp only: supp_at_base)
+apply(simp)
 done
 
 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
 
+ML {* val _ = recursive := true *}
+
+nominal_datatype lam' =
+  VAR' "name"
+| APP' "lam'" "lam'"
+| LAM' x::"name" t::"lam'"  bind x in t
+| LET' bp::"bp'" t::"lam'"   bind "bi' bp" in t
+and bp' =
+  BP' "name" "lam'"
+binder
+  bi'::"bp' \<Rightarrow> atom set"
+where
+  "bi' (BP' x t) = {atom x}"
+
+thm lam'_bp'_fv
+thm lam'_bp'_inject[no_vars]
+thm lam'_bp'_bn
+thm lam'_bp'_perm
+thm lam'_bp'_induct
+thm lam'_bp'_inducts
+thm lam'_bp'_distinct
+ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
+
+lemma supp_fv:
+  shows "supp t = fv_lam' t" 
+  and "supp bp = fv_bp' bp"
+apply(induct t and bp rule: lam'_bp'_inducts)
+apply(simp_all add: lam'_bp'_fv)
+(* VAR case *)
+apply(simp only: supp_def)
+apply(simp only: lam'_bp'_perm)
+apply(simp only: lam'_bp'_inject)
+apply(simp only: supp_def[symmetric])
+apply(simp only: supp_at_base)
+(* APP case *)
+apply(simp only: supp_def)
+apply(simp only: lam'_bp'_perm)
+apply(simp only: lam'_bp'_inject)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: infinite_Un)
+apply(simp only: Collect_disj_eq)
+(* LAM case *)
+apply(rule_tac t="supp (LAM' name lam'_raw)" and s="supp (Abs {atom name} lam'_raw)" in subst)
+apply(simp (no_asm) only: supp_def)
+apply(simp only: lam'_bp'_perm)
+apply(simp only: permute_ABS)
+apply(simp only: lam'_bp'_inject)
+apply(simp only: Abs_eq_iff)
+apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
+apply(simp only: alpha_gen)
+apply(simp only: supp_eqvt[symmetric])
+apply(simp only: eqvts)
+apply(simp only: supp_Abs)
+(* LET case *)
+apply(rule_tac t="supp (LET' bp'_raw lam'_raw)" and 
+               s="supp (Abs (bi' bp'_raw) (bp'_raw, lam'_raw))" in subst)
+apply(simp (no_asm) only: supp_def)
+apply(simp only: lam'_bp'_perm)
+apply(simp only: permute_ABS)
+apply(simp only: lam'_bp'_inject)
+apply(simp only: eqvts)
+apply(simp only: Abs_eq_iff)
+apply(rule Collect_cong)
+apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+apply(simp)
+apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+apply(simp)
+apply(rule Collect_cong)
+apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+apply(simp)
+apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+apply(simp)
+apply(rule ext)
+apply(rule sym)
+apply(subgoal_tac "fv_bp' = supp")
+apply(subgoal_tac "fv_lam' = supp")
+apply(simp)
+apply(rule trans)
+apply(rule alpha_abs_Pair[symmetric])
+apply(simp add: alpha_gen supp_Pair)
+oops
+
+thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
+
+
 text {* example 2 *}
 
+ML {* val _ = recursive := false  *}
 nominal_datatype trm' =
   Var "name"
 | App "trm'" "trm'"
@@ -134,11 +219,82 @@
 thm trm'_pat'_induct
 thm trm'_pat'_distinct
 
-(* compat should be
-compat (PN) pi (PN) == True
-compat (PS x) pi (PS x') == pi o x = x'
-compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2'
-*)
+lemma supp_fv_trm'_pat':
+  shows "supp t = fv_trm' t" 
+  and "supp bp = fv_pat' bp \<and> {a. infinite {b. \<not>alpha_f ((a \<rightleftharpoons> b) \<bullet> bp) bp}} = fv_f bp"
+apply(induct t and bp rule: trm'_pat'_inducts)
+apply(simp_all add: trm'_pat'_fv)
+(* VAR case *)
+apply(simp only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'_inject)
+apply(simp only: supp_def[symmetric])
+apply(simp only: supp_at_base)
+(* APP case *)
+apply(simp only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'_inject)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: infinite_Un)
+apply(simp only: Collect_disj_eq)
+(* LAM case *)
+apply(rule_tac t="supp (Lam name trm'_raw)" and s="supp (Abs {atom name} trm'_raw)" in subst)
+apply(simp (no_asm) only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: permute_ABS)
+apply(simp only: trm'_pat'_inject)
+apply(simp only: Abs_eq_iff)
+apply(simp only: insert_eqvt atom_eqvt empty_eqvt)
+apply(simp only: alpha_gen)
+apply(simp only: supp_eqvt[symmetric])
+apply(simp only: eqvts)
+apply(simp only: supp_Abs)
+(* LET case *)
+apply(rule_tac t="supp (Let pat'_raw trm'_raw1 trm'_raw2)" 
+           and s="supp (Abs (f pat'_raw) trm'_raw2) \<union> supp trm'_raw1 \<union> fv_f pat'_raw" in subst)
+apply(simp (no_asm) only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: permute_ABS)
+apply(simp only: trm'_pat'_inject)
+apply(simp only: eqvts)
+apply(simp only: Abs_eq_iff)
+apply(simp only: ex_simps)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: infinite_Un)
+apply(simp only: Collect_disj_eq)
+apply(simp only: alpha_gen)
+apply(simp only: supp_eqvt[symmetric])
+apply(simp only: eqvts)
+apply(blast)
+apply(simp add: supp_Abs)
+apply(blast)
+(* PN case *)
+apply(simp only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'_inject)
+apply(simp)
+(* PS case *)
+apply(simp only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'_inject)
+apply(simp only: supp_def[symmetric])
+apply(simp only: supp_at_base)
+apply(simp)
+(* PD case *)
+apply(simp only: supp_def)
+apply(simp only: trm'_pat'_perm)
+apply(simp only: trm'_pat'_inject)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: infinite_Un)
+apply(simp only: Collect_disj_eq)
+apply(simp only: supp_def[symmetric])
+apply(simp add: supp_at_base)
+done
+
+thm trm'_pat'_fv[simplified supp_fv_trm'_pat'(1)[symmetric] supp_fv_trm'_pat'(2)[THEN conjunct1, symmetric]]
 
 nominal_datatype trm0 =
   Var0 "name"
@@ -340,17 +496,17 @@
   VarP "name"
 | AppP "exp" "exp"
 | LamP x::"name" e::"exp" bind x in e
-| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp' p" in e1
+| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp'' p" in e1
 and pat3 =
   PVar "name"
 | PUnit
 | PPair "pat3" "pat3"
 binder
-  bp' :: "pat3 \<Rightarrow> atom set"
+  bp'' :: "pat3 \<Rightarrow> atom set"
 where
-  "bp' (PVar x) = {atom x}"
-| "bp' (PUnit) = {}"
-| "bp' (PPair p1 p2) = bp' p1 \<union> bp' p2"
+  "bp'' (PVar x) = {atom x}"
+| "bp'' (PUnit) = {}"
+| "bp'' (PPair p1 p2) = bp'' p1 \<union> bp'' p2"
 
 thm exp_pat3_fv
 thm exp_pat3_inject
@@ -385,16 +541,17 @@
 (* THE REST ARE NOT SUPPOSED TO WORK YET *)
 
 (* example 7 from Peter Sewell's bestiary *)
+(* dest_Const raised
 nominal_datatype exp7 =
-  EVar name
-| EUnit
-| EPair exp7 exp7
-| ELetRec l::lrbs e::exp7 bind "b7s l" in e, bind "b7s l" in l
+  EVar' name
+| EUnit'
+| EPair' exp7 exp7
+| ELetRec' l::lrbs e::exp7 bind "b7s l" in e, bind "b7s l" in l
 and lrb =
-  Assign name exp7
+  Assign' name exp7
 and lrbs =
-  Single lrb
-| More lrb lrbs
+  Single' lrb
+| More' lrb lrbs
 binder
   b7 :: "lrb \<Rightarrow> atom set" and
   b7s :: "lrbs \<Rightarrow> atom set"
@@ -403,27 +560,31 @@
 | "b7s (Single a) = b7 a"
 | "b7s (More a as) = (b7 a) \<union> (b7s as)"
 thm alpha_exp7_raw_alpha_lrb_raw_alpha_lrbs_raw.intros
+*)
 
 (* example 8 from Peter Sewell's bestiary *)
+(*
+*** fv_bn: recursive argument, but wrong datatype.
+*** At command "nominal_datatype".
 nominal_datatype exp8 =
-  EVar name
-| EUnit
-| EPair exp8 exp8
-| ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e, bind "b_lrbs8 l" in l
+  EVar' name
+| EUnit'
+| EPair' exp8 exp8
+| ELetRec' l::lrbs8 e::exp8 bind "b_lrbs8 l" in e, bind "b_lrbs8 l" in l
 and fnclause =
-  K x::name p::pat8 e::exp8 bind "b_pat p" in e
+  K' x::name p::pat8 e::exp8 bind "b_pat p" in e
 and fnclauses =
-  S fnclause
-| ORs fnclause fnclauses
+  S' fnclause
+| ORs' fnclause fnclauses
 and lrb8 =
-  Clause fnclauses
+  Clause' fnclauses
 and lrbs8 =
-  Single lrb8
-| More lrb8 lrbs8
+  Single' lrb8
+| More' lrb8 lrbs8
 and pat8 =
-  PVar name
-| PUnit
-| PPair pat8 pat8
+  PVar'' name
+| PUnit''
+| PPair'' pat8 pat8
 binder
   b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and
   b_pat :: "pat8 \<Rightarrow> atom set" and
@@ -431,20 +592,21 @@
   b_fnclause :: "fnclause \<Rightarrow> atom set" and
   b_lrb8 :: "lrb8 \<Rightarrow> atom set"
 where
-  "b_lrbs8 (Single l) = b_lrb8 l"
-| "b_lrbs8 (More l ls) = b_lrb8 l \<union> b_lrbs8 ls"
-| "b_pat (PVar x) = {atom x}"
-| "b_pat (PUnit) = {}"
-| "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
-| "b_fnclauses (S fc) = (b_fnclause fc)"
-| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
-| "b_lrb8 (Clause fcs) = (b_fnclauses fcs)"
-| "b_fnclause (K x pat exp8) = {atom x}"
+  "b_lrbs8 (Single' l) = b_lrb8 l"
+| "b_lrbs8 (More' l ls) = b_lrb8 l \<union> b_lrbs8 ls"
+| "b_pat (PVar'' x) = {atom x}"
+| "b_pat (PUnit'') = {}"
+| "b_pat (PPair'' p1 p2) = b_pat p1 \<union> b_pat p2"
+| "b_fnclauses (S' fc) = (b_fnclause fc)"
+| "b_fnclauses (ORs' fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
+| "b_lrb8 (Clause' fcs) = (b_fnclauses fcs)"
+| "b_fnclause (K' x pat exp8) = {atom x}"
 thm alpha_exp8_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb8_raw_alpha_lrbs8_raw_alpha_pat8_raw.intros
-
+*)
 (* example 4 from Terms.thy *)
 (* fv_eqvt does not work, we need to repaire defined permute functions
    defined fv and defined alpha... *)
+(* lists-datastructure does not work yet
 nominal_datatype trm4 =
   Vr4 "name"
 | Ap4 "trm4" "trm4 list"
@@ -452,12 +614,13 @@
 
 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
-
+*)
 (* core haskell *)
 atom_decl var
 atom_decl tvar
 
 (* there are types, coercion types and regular types *)
+(* list-data-structure
 nominal_datatype tkind =
   KStar
 | KFun "tkind" "tkind"
@@ -485,13 +648,6 @@
 | CLeftc "co"
 | CCoe "co" "co"
 
-
-typedecl ty --"hack since ty is not yet defined"
-typedecl kind
-
-instance ty and kind:: pt
-sorry
-
 abbreviation
   "atoms A \<equiv> atom ` A"
 
@@ -513,15 +669,8 @@
  bv :: "pat \<Rightarrow> atom set"
 where
  "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
-
-(*
-compat (K s ts vs) pi (K s' ts' vs') ==
-  s = s' &
-
 *)
 
-
-
 text {* weirdo example from Peter Sewell's bestiary *}
 
 nominal_datatype weird =
@@ -537,6 +686,7 @@
 (* example 6 from Terms.thy *)
 
 (* BV is not respectful, needs to fail*)
+(*
 nominal_datatype trm6 =
   Vr6 "name"
 | Lm6 x::"name" t::"trm6"         bind x in t
@@ -547,9 +697,11 @@
   "bv6 (Vr6 n) = {}"
 | "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
 | "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
-(* example 7 from Terms.thy *)
+*)
 
+(* example 7 from Terms.thy *)
 (* BV is not respectful, needs to fail*)
+(*
 nominal_datatype trm7 =
   Vr7 "name"
 | Lm7 l::"name" r::"trm7"   bind l in r
@@ -560,10 +712,12 @@
   "bv7 (Vr7 n) = {atom n}"
 | "bv7 (Lm7 n t) = bv7 t - {atom n}"
 | "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
+*)
 
 (* example 8 from Terms.thy *)
 
 (* Binding in a term under a bn, needs to fail *)
+(*
 nominal_datatype foo8 =
   Foo0 "name"
 | Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo"
@@ -575,10 +729,11 @@
 where
   "bv8 (Bar0 x) = {}"
 | "bv8 (Bar1 v x b) = {atom v}"
-
+*)
 (* example 9 from Terms.thy *)
 
 (* BV is not respectful, needs to fail*)
+(*
 nominal_datatype lam9 =
   Var9 "name"
 | Lam9 n::"name" l::"lam9" bind n in l
@@ -589,18 +744,20 @@
 where
   "bv9 (Var9 x) = {}"
 | "bv9 (Lam9 x b) = {atom x}"
-
+*)
 
 (* Type schemes with separate datatypes *)
-nominal_datatype t =
-  Var "name"
-| Fun "t" "t"
+nominal_datatype T =
+  TVar "name"
+| TFun "T" "T"
 
-nominal_datatype tyS =
-  All xs::"name list" ty::"t_raw" bind xs in ty
-
-
-
+(* PROBLEM: 
+*** exception Datatype raised 
+*** (line 218 of "/usr/local/src/Isabelle_16-Mar-2010/src/HOL/Tools/Datatype/datatype_aux.ML")
+*** At command "nominal_datatype".
+nominal_datatype TyS =
+  TAll xs::"name list" ty::"T" bind xs in ty
+*)
 
 (* example 9 from Peter Sewell's bestiary *)
 (* run out of steam at the moment *)