--- a/Quot/QuotList.thy	Mon Jan 25 19:52:53 2010 +0100
+++ b/Quot/QuotList.thy	Mon Jan 25 20:35:42 2010 +0100
@@ -192,13 +192,9 @@
 apply(simp_all)
 done
 
-
-(* Rest are unused *)
-text {*
 lemma list_rel_refl:
   assumes a: "\<And>x y. R x y = (R x = R y)"
   shows "list_rel R x x"
 by (induct x) (auto simp add: a)
-*}
 
 end