diff -r 8441b4b2469d -r a69ec3f3f535 Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Tue Feb 09 15:20:40 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Tue Feb 09 15:20:52 2010 +0100
@@ -227,7 +227,6 @@
 
 (* TEST case *)
 lemmas abs_induct2 = prod.induct[where 'a="atom set" and 'b="'a::pt", quot_lifted]
-
 thm abs_induct abs_induct2
 
 instantiation abs :: (pt) pt