
diff -r 6b2f6e7e62cc -r d2c9a72e52e0 QuotMain.thy
--- 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, ...} =>




