--- a/Quot/QuotMain.thy	Tue Dec 22 20:51:37 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 22 21:06:46 2009 +0100
@@ -110,6 +110,11 @@
   id_o[THEN eq_reflection]
   o_id[THEN eq_reflection] 
 
+
+(* The translation functions for the lifting process. *)
+use "quotient_term.ML" 
+
+
 (* Definition of the quotient types *)
 use "quotient_typ.ML"
 
@@ -117,11 +122,6 @@
 (* Definitions for quotient constants *)
 use "quotient_def.ML"
 
-
-(* The translation functions for the lifting process. *)
-use "quotient_term.ML" 
-
-
 (* Tactics for proving the lifted theorems *)
 
 lemma eq_imp_rel: