diff -r e2ac18492c68 -r baac4639ecef Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Sat Dec 19 22:09:57 2009 +0100
+++ b/Quot/quotient_tacs.ML	Sat Dec 19 22:21:51 2009 +0100
@@ -11,6 +11,11 @@
 structure Quotient_Tacs: QUOTIENT_TACS =
 struct
 
+open Quotient_Info;
+open Quotient_Type;
+open Quotient_Term;
+
+
 (* Since HOL_basic_ss is too "big" for us,    *)
 (* we need to set up our own minimal simpset. *)
 fun  mk_minimal_ss ctxt =
@@ -563,8 +568,6 @@
 in
   error msg
 end
-
-open Quotient_Term;
  
 fun procedure_inst ctxt rtrm qtrm =
 let
@@ -615,6 +618,4 @@
       (all_inj_repabs_tac ctxt, msg2),
       (clean_tac ctxt, msg3)]
 
-
-
-end;
\ No newline at end of file
+end; (* structure *)
\ No newline at end of file