--- a/Nominal/Ex/TypeVarsTest.thy	Sat Jan 11 23:17:23 2014 +0000
+++ b/Nominal/Ex/TypeVarsTest.thy	Mon Jan 13 15:42:10 2014 +0000
@@ -27,6 +27,7 @@
 term Foo
 term Bar
 
+thm lam.supp lam.fresh
 thm lam.distinct
 thm lam.induct
 thm lam.exhaust 
@@ -43,6 +44,7 @@
   PsiNil
 | Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" 
 
+thm psi.supp psi.fresh
 
 nominal_datatype 'a foo = 
   Node x::"name" f::"'a foo" binds x in f