--- a/Nominal/Ex/SystemFOmega.thy	Tue Dec 21 10:28:08 2010 +0000
+++ b/Nominal/Ex/SystemFOmega.thy	Wed Dec 22 09:13:25 2010 +0000
@@ -18,9 +18,9 @@
 nominal_datatype ty =
   TVar tvar
 | TFun ty ty
-| TAll a::tvar kind t::ty bind a in t
-| TEx  a::tvar kind t::ty bind a in t
-| TLam a::tvar kind t::ty bind a in t
+| TAll a::tvar kind t::ty  bind a in t
+| TEx  a::tvar kind t::ty  bind a in t
+| TLam a::tvar kind t::ty  bind a in t
 | TApp ty ty
 | TRec trec
 and trec =
@@ -29,20 +29,50 @@
 
 nominal_datatype trm =
   Var var
-| Lam x::var ty t::trm bind x in t
+| Lam x::var ty t::trm  bind x in t
 | App trm trm
 | Dot trm label
-| LAM a::tvar kind t::trm bind a in t
+| LAM a::tvar kind t::trm  bind a in t
 | APP trm ty
 | Pack ty trm
-| Unpack a::tvar x::var trm t::trm bind a x in t
+| Unpack a::tvar x::var trm t::trm  bind a x in t
 | Rec rec 
 and rec =
   RNil
 | RCons label trm rec
 
 
+thm ty_trec.distinct
+thm ty_trec.induct
+thm ty_trec.inducts
+thm ty_trec.exhaust 
+thm ty_trec.strong_exhaust
+thm ty_trec.fv_defs
+thm ty_trec.bn_defs
+thm ty_trec.perm_simps
+thm ty_trec.eq_iff
+thm ty_trec.fv_bn_eqvt
+thm ty_trec.size_eqvt
+thm ty_trec.supports
+thm ty_trec.fsupp
+thm ty_trec.supp
+thm ty_trec.fresh
 
+thm trm_rec.distinct
+thm trm_rec.induct
+thm trm_rec.inducts
+thm trm_rec.exhaust
+thm trm_rec.strong_exhaust
+thm trm_rec.fv_defs
+thm trm_rec.bn_defs
+thm trm_rec.perm_simps
+thm trm_rec.eq_iff
+thm trm_rec.fv_bn_eqvt
+thm trm_rec.size_eqvt
+thm trm_rec.supports
+thm trm_rec.fsupp
+thm trm_rec.supp
+thm trm_rec.fresh
 
 end