--- a/QuotMain.thy	Mon Nov 23 23:09:03 2009 +0100
+++ b/QuotMain.thy	Tue Nov 24 01:36:50 2009 +0100
@@ -1374,13 +1374,11 @@
 (* rep-abs injection *)
 
 ML {*
-(* FIXME: is this the right get_fun function for rep-abs injection *)
 fun mk_repabs lthy (T, T') trm = 
   Quotient_Def.get_fun repF lthy (T, T') 
-  $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
+    $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
 *}
 
-ML {* length *}
 
 ML {*
 (* bound variables need to be treated properly,  *)