--- a/Quot/Nominal/Fv.thy	Mon Feb 22 10:39:05 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Mon Feb 22 10:57:39 2010 +0100
@@ -90,6 +90,8 @@
 
 *}
 
+(* TODO: Notice datatypes without bindings and replace alpha with equality *)
+
 ML {*
 (* Currently needs just one full_tname to access Datatype *)
 fun define_fv_alpha full_tname bindsall lthy =

--- a/Quot/Nominal/Terms.thy	Mon Feb 22 10:39:05 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Mon Feb 22 10:57:39 2010 +0100
@@ -342,86 +342,85 @@
 
 section {*** lets with many assignments ***}
 
-datatype trm3 =
-  Vr3 "name"
-| Ap3 "trm3" "trm3"
-| Lm3 "name" "trm3" --"bind (name) in (trm3)"
-| Lt3 "assigns" "trm3" --"bind (bv3 assigns) in (trm3)"
-and assigns =
-  ANil
-| ACons "name" "trm3" "assigns"
+datatype rtrm3 =
+  rVr3 "name"
+| rAp3 "rtrm3" "rtrm3"
+| rLm3 "name" "rtrm3" --"bind (name) in (trm3)"
+| rLt3 "rassigns" "rtrm3" --"bind (bv3 assigns) in (trm3)"
+and rassigns =
+  rANil
+| rACons "name" "rtrm3" "rassigns"
 
 (* to be given by the user *)
 primrec 
   bv3
 where
-  "bv3 ANil = {}"
-| "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
+  "bv3 rANil = {}"
+| "bv3 (rACons x t as) = {atom x} \<union> (bv3 as)"
 
-setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *}
+setup {* snd o define_raw_perms ["rtrm3", "rassigns"] ["Terms.rtrm3", "Terms.rassigns"] *}
 
-local_setup {* snd o define_fv_alpha "Terms.trm3"
+local_setup {* snd o define_fv_alpha "Terms.rtrm3"
   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]],
    [[], [[], [], []]]] *}
 print_theorems
 
 notation
-  alpha_trm3 ("_ \<approx>3 _" [100, 100] 100) and
-  alpha_assigns ("_ \<approx>3a _" [100, 100] 100)
-thm alpha_trm3_alpha_assigns.intros
+  alpha_rtrm3 ("_ \<approx>3 _" [100, 100] 100) and
+  alpha_rassigns ("_ \<approx>3a _" [100, 100] 100)
+thm alpha_rtrm3_alpha_rassigns.intros
 
 lemma alpha3_equivp:
-  "equivp alpha_trm3"
-  "equivp alpha_assigns"
+  "equivp alpha_rtrm3"
+  "equivp alpha_rassigns"
   sorry
 
 quotient_type
-  qtrm3 = trm3 / alpha_trm3
+  trm3 = rtrm3 / alpha_rtrm3
 and
-  qassigns = assigns / alpha_assigns
+  assigns = rassigns / alpha_rassigns
   by (auto intro: alpha3_equivp)
 
 
 section {*** lam with indirect list recursion ***}
 
-datatype trm4 =
-  Vr4 "name"
-| Ap4 "trm4" "trm4 list"
-| Lm4 "name" "trm4"  --"bind (name) in (trm)"
-print_theorems
+datatype rtrm4 =
+  rVr4 "name"
+| rAp4 "rtrm4" "rtrm4 list"
+| rLm4 "name" "rtrm4"  --"bind (name) in (trm)"
 
-thm trm4.recs
+thm rtrm4.recs
 
 (* there cannot be a clause for lists, as *)
 (* permutations are  already defined in Nominal (also functions, options, and so on) *)
-setup {* snd o define_raw_perms ["trm4"] ["Terms.trm4"] *}
+setup {* snd o define_raw_perms ["rtrm4"] ["Terms.rtrm4"] *}
 
 (* "repairing" of the permute function *)
 lemma repaired:
-  fixes ts::"trm4 list"
-  shows "permute_trm4_list p ts = p \<bullet> ts"
+  fixes ts::"rtrm4 list"
+  shows "permute_rtrm4_list p ts = p \<bullet> ts"
   apply(induct ts)
   apply(simp_all)
   done
 
-thm permute_trm4_permute_trm4_list.simps
-thm permute_trm4_permute_trm4_list.simps[simplified repaired]
+thm permute_rtrm4_permute_rtrm4_list.simps
+thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
 
-local_setup {* snd o define_fv_alpha "Terms.trm4" [
+local_setup {* snd o define_fv_alpha "Terms.rtrm4" [
   [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]]  ] *}
 print_theorems
 
 notation
-  alpha_trm4 ("_ \<approx>4 _" [100, 100] 100) and
-  alpha_trm4_list ("_ \<approx>4l _" [100, 100] 100)
-thm alpha_trm4_alpha_trm4_list.intros
+  alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and
+  alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
+thm alpha_rtrm4_alpha_rtrm4_list.intros
 
-lemma alpha4_equivp: "equivp alpha_trm4" sorry
-lemma alpha4list_equivp: "equivp alpha_trm4_list" sorry
+lemma alpha4_equivp: "equivp alpha_rtrm4" sorry
+lemma alpha4list_equivp: "equivp alpha_rtrm4_list" sorry
 
 quotient_type 
-  qtrm4 = trm4 / alpha_trm4 and
-  qtrm4list = "trm4 list" / alpha_trm4_list
+  qrtrm4 = rtrm4 / alpha_rtrm4 and
+  qrtrm4list = "rtrm4 list" / alpha_rtrm4_list
   by (simp_all add: alpha4_equivp alpha4list_equivp)