--- a/Nominal/Test.thy	Thu Mar 11 16:50:44 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 11 17:47:29 2010 +0100
@@ -4,6 +4,8 @@
 
 text {* example 1, equivalent to example 2 from Terms *}
 
+atom_decl name
+
 nominal_datatype lam =
   VAR "name"
 | APP "lam" "lam"
@@ -21,6 +23,9 @@
 thm lam_bp_perm
 thm lam_bp_induct
 thm lam_bp_distinct
+ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
+
+term "supp (x :: lam)"
 
 (* compat should be
 compat (BP x t) pi (BP x' t')