diff -r 66097fe4942a -r de2d1929899f Quot/Nominal/Abs.thy --- 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