--- a/Quot/QuotMain.thy	Thu Jan 14 10:06:29 2010 +0100
+++ b/Quot/QuotMain.thy	Thu Jan 14 10:47:19 2010 +0100
@@ -148,30 +148,6 @@
 use "quotient_tacs.ML"
 
 
-(* Atomize infrastructure *)
-(* FIXME/TODO: is this really needed? *)
-(*
-lemma atomize_eqv[atomize]:
-  shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
-proof
-  assume "A \<equiv> B"
-  then show "Trueprop A \<equiv> Trueprop B" by unfold
-next
-  assume *: "Trueprop A \<equiv> Trueprop B"
-  have "A = B"
-  proof (cases A)
-    case True
-    have "A" by fact
-    then show "A = B" using * by simp
-  next
-    case False
-    have "\<not>A" by fact
-    then show "A = B" using * by auto
-  qed
-  then show "A \<equiv> B" by (rule eq_reflection)
-qed
-*)
-
 section {* Methods / Interface *}
 
 ML {*

--- a/Quot/quotient_tacs.ML	Thu Jan 14 10:06:29 2010 +0100
+++ b/Quot/quotient_tacs.ML	Thu Jan 14 10:47:19 2010 +0100
@@ -57,7 +57,7 @@
 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
 
-fun quotient_tac ctxt = SOLVED'
+fun quotient_tac ctxt =
   (REPEAT_ALL_NEW (FIRST'
     [rtac @{thm identity_quotient},
      resolve_tac (quotient_rules_get ctxt)]))

--- a/Unused.thy	Thu Jan 14 10:06:29 2010 +0100
+++ b/Unused.thy	Thu Jan 14 10:47:19 2010 +0100
@@ -7,6 +7,30 @@
 
 
 
+(* Atomize infrastructure *)
+(* FIXME/TODO: is this really needed? *)
+(*
+lemma atomize_eqv:
+  shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
+proof
+  assume "A \<equiv> B"
+  then show "Trueprop A \<equiv> Trueprop B" by unfold
+next
+  assume *: "Trueprop A \<equiv> Trueprop B"
+  have "A = B"
+  proof (cases A)
+    case True
+    have "A" by fact
+    then show "A = B" using * by simp
+  next
+    case False
+    have "\<not>A" by fact
+    then show "A = B" using * by auto
+  qed
+  then show "A \<equiv> B" by (rule eq_reflection)
+qed
+*)
+
 
 ML {*
   fun dest_cbinop t =