diff -r ec37a279ca55 -r 018aabbffd08 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Mon Dec 07 23:45:51 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 01:00:21 2009 +0100
@@ -144,8 +144,7 @@
 
 declare [[map * = (prod_fun, prod_rel)]]
 declare [[map "fun" = (fun_map, fun_rel)]]
-
-(* FIXME: This should throw an exception: *)
+(* Throws now an exception:              *)
 (* declare [[map "option" = (bla, blu)]] *)
 
 
@@ -161,9 +160,6 @@
 lemmas [quotient_equiv] =
   identity_equivp prod_equivp
 
-ML {* maps_lookup @{theory} "*" *}
-ML {* maps_lookup @{theory} "fun" *}
-
 
 (* definition of the quotient types *)
 (* FIXME: should be called quotient_typ.ML *)