--- a/Nominal/Ex/Lambda.thy	Sun Jun 05 16:58:18 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Sun Jun 05 21:14:23 2011 +0100
@@ -35,6 +35,7 @@
   and "sort_of (atom x) = sort_of (atom y)"
   shows "f x T = f y S"
 using assms apply -
+thm Abs1_eq_iff'
 apply (subst (asm) Abs1_eq_iff')
 apply simp_all
 apply (elim conjE disjE)
@@ -62,7 +63,7 @@
        and fcb: "\<forall>x t r. atom x \<sharp> f3 x t r"
 begin
 
-nominal_primrec
+nominal_primrec 
   f :: "lam \<Rightarrow> ('a::pt)"
 where
   "f (Var x) = f1 x"
@@ -92,7 +93,9 @@
 
 end
 
+
 thm test.f.simps
+thm test.f.simps[simplified test_def]
 
 thm test_def