--- a/Quot/QuotList.thy	Mon Jan 25 18:52:22 2010 +0100
+++ b/Quot/QuotList.thy	Mon Jan 25 19:14:46 2010 +0100
@@ -161,7 +161,7 @@
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl"
-apply auto
+apply(auto)
 apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)")
 apply simp
 apply (rule_tac x="xa" in spec)
@@ -192,11 +192,13 @@
 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