--- a/Quot/Examples/LFex.thy Thu Dec 10 03:48:39 2009 +0100 +++ b/Quot/Examples/LFex.thy Thu Dec 10 04:23:13 2009 +0100 @@ -80,8 +80,6 @@ and TRM = trm / atrm by (auto intro: alpha_equivps) -print_quotients - quotient_def TYP :: "TYP :: KIND" where