--- a/Nominal/Ex/Datatypes.thy	Sun Jun 19 13:10:15 2011 +0900
+++ b/Nominal/Ex/Datatypes.thy	Sun Jun 19 13:14:37 2011 +0900
@@ -56,6 +56,7 @@
   Baz x::name t::foo bind x in t
 
 
+
 thm baz.distinct
 thm baz.induct
 thm baz.exhaust
@@ -78,7 +79,7 @@
 | Fun "nat \<Rightarrow> nat"
 | Var "name"
 | Lam x::"name" t::"set_ty" bind x in t
-
+thm meta_eq_to_obj_eq
 thm set_ty.distinct
 thm set_ty.induct
 thm set_ty.exhaust