--- a/Quot/Nominal/Abs.thy Mon Feb 08 13:50:52 2010 +0100
+++ b/Quot/Nominal/Abs.thy Tue Feb 09 10:48:42 2010 +0100
@@ -226,7 +226,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