--- a/Quot/QuotMain.thy	Mon Jan 25 17:53:08 2010 +0100
+++ b/Quot/QuotMain.thy	Mon Jan 25 18:13:44 2010 +0100
@@ -3,7 +3,7 @@
 *)
 
 theory QuotMain
-imports QuotScript Prove
+imports QuotBase
 uses ("quotient_info.ML")
      ("quotient_typ.ML")
      ("quotient_def.ML")
@@ -61,11 +61,6 @@
   show "Abs (R (Eps (Rep a))) = a" by simp
 qed
 
-lemma rep_refl:
-  shows "R (rep a) (rep a)"
-unfolding rep_def
-by (simp add: equivp[simplified equivp_def])
-
 lemma lem7:
   shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS")
 proof -
@@ -79,6 +74,12 @@
 unfolding abs_def
 by (simp only: equivp[simplified equivp_def] lem7)
 
+lemma rep_refl:
+  shows "R (rep a) (rep a)"
+unfolding rep_def
+by (simp add: equivp[simplified equivp_def])
+
+
 lemma rep_abs_rsp:
   shows "R f (rep (abs g)) = R f g"
   and   "R (rep (abs g)) f = R g f"