--- a/Nominal/Fv.thy	Mon Mar 08 11:25:57 2010 +0100
+++ b/Nominal/Fv.thy	Mon Mar 08 14:31:04 2010 +0100
@@ -58,6 +58,12 @@
   body.
 *)
 
+ML {*
+fun is_atom thy typ =
+  Sign.of_sort thy (typ, @{sort at})
+*}
+
+
 (* Like map2, only if the second list is empty passes empty lists insted of error *)
 ML {*
 fun map2i _ [] [] = []

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Term5a.thy	Mon Mar 08 14:31:04 2010 +0100
@@ -0,0 +1,38 @@
+theory Term5
+imports "Parser"
+begin
+
+atom_decl name
+
+ML {* restricted_nominal := 2 *}
+
+nominal_datatype trm5 =
+  Vr5 "name"
+| Ap5 "trm5" "trm5"
+| Lt5 l::"lts" t::"trm5"  bind "bv5 l" in t
+and lts =
+  Lnil
+| Lcons "name" "trm5" "lts"
+binder
+  bv5
+where
+  "bv5 Lnil = {}"
+| "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"
+
+lemma lets_ok:
+  "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
+apply (simp add: trm5_lts_inject)
+apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+apply (simp_all add: alpha_gen)
+apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn)
+done
+
+lemma lets_nok:
+  "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons y (Vr5 x) Lnil) (Vr5 y))"
+apply (simp only: trm5_lts_inject not_ex)
+apply (rule allI)
+apply (simp add: alpha_gen)
+apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn trm5_lts_inject)
+done
+
+end