--- a/Nominal/Ex/Datatypes.thy	Thu Jun 16 23:11:50 2011 +0900
+++ b/Nominal/Ex/Datatypes.thy	Thu Jun 16 20:07:03 2011 +0100
@@ -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