diff -r 8cf5c3e58889 -r 8ed62410236e Nominal-General/Atoms.thy
--- a/Nominal-General/Atoms.thy	Fri Nov 05 15:21:10 2010 +0000
+++ b/Nominal-General/Atoms.thy	Sat Nov 06 06:18:41 2010 +0000
@@ -5,6 +5,7 @@
 *)
 theory Atoms
 imports Nominal2_Base
+uses "~~/src/Tools/subtyping.ML"
 begin
 
 
@@ -193,4 +194,29 @@
   unfolding atom_eqvt [symmetric]
   by simp
 
+
+section {* Tests with subtyping and automatic coercions *}
+
+setup Subtyping.setup
+
+atom_decl var1
+atom_decl var2
+
+declare [[coercion "atom::var1\<Rightarrow>atom"]]
+
+declare [[coercion "atom::var2\<Rightarrow>atom"]]
+
+lemma
+  fixes a::"var1" and b::"var2"
+  shows "a \<sharp> t \<and> b \<sharp> t"
+oops
+
+(* does not yet work: it needs image as
+   coercion map *)
+
+lemma
+  fixes as::"var1 set"
+  shows "atom ` as \<sharp>* t"
+oops
+
 end