--- 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