diff -r 120e479ed367 -r 38aa6b67a80b Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Mon Dec 07 17:57:33 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 07 18:49:14 2009 +0100
@@ -588,7 +588,6 @@
   (* can this cause loops in equiv_tac ? *)
   val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
 in
-  ObjectLogic.full_atomize_tac THEN'
   simp_tac simpset THEN'
   REPEAT_ALL_NEW (CHANGED o FIRST' [
     rtac @{thm ball_reg_right},
@@ -597,8 +596,9 @@
     rtac @{thm ball_all_comm},
     rtac @{thm bex_ex_comm},
     resolve_tac eq_eqvs,  
-    (* should be equivalent to the above, but causes loops: *) 
+    (* should be equivalent to the above, but causes loops:   *) 
     (* rtac @{thm eq_imp_rel} THEN' SOLVES' (equiv_tac ctxt), *)
+    (* the culprit is aslread rtac @{thm eq_imp_rel}          *)
     simp_tac simpset])
 end
 *}
@@ -1133,7 +1133,7 @@
 
 lemma lifting_procedure:
   assumes a: "A"
-  and     b: "A \<Longrightarrow> B"
+  and     b: "A \<longrightarrow> B"
   and     c: "B = C"
   and     d: "C = D"
   shows   "D"