--- a/Nominal/Ex/Foo2.thy	Fri Dec 10 19:01:44 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Sun Dec 12 00:10:40 2010 +0000
@@ -24,9 +24,10 @@
  "bn (As x y t a) = [atom x] @ bn a"
 | "bn (As_Nil) = []"
 
-term "bn"
-
-
+ML {* 
+  Variable.import;
+  Variable.import true @{thms foo.exhaust} @{context}
+*}
 
 thm foo.bn_defs
 thm foo.permute_bn
@@ -42,7 +43,7 @@
 thm foo.fv_defs
 thm foo.bn_defs
 thm foo.perm_simps
-thm foo.eq_iff(5)
+thm foo.eq_iff
 thm foo.fv_bn_eqvt
 thm foo.size_eqvt
 thm foo.supports
@@ -52,6 +53,7 @@
 
 
 
+text {* *}