--- a/QuotMain.thy	Thu Dec 03 11:40:10 2009 +0100
+++ b/QuotMain.thy	Thu Dec 03 13:59:53 2009 +0100
@@ -716,7 +716,7 @@
 section {* RepAbs Injection Tactic *}
 
 (* TODO: check if it still works with first_order_match *)
-(* FIXME/TODO: do not handle everything *)x
+(* FIXME/TODO: do not handle everything *)
 ML {*
 fun instantiate_tac thm = 
   Subgoal.FOCUS (fn {concl, ...} =>