diff -r e903c32ec24f -r 693562f03eee Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Wed Oct 13 22:55:58 2010 +0100 +++ b/Nominal/Ex/SingleLet.thy Thu Oct 14 04:14:22 2010 +0100 @@ -157,10 +157,7 @@ apply(simp add: finite_supp) apply(simp add: finite_supp) oops - (*apply(simp add: Abs_fresh_star)*) -sorry - -done + end