--- a/QuotMain.thy	Mon Nov 02 18:16:19 2009 +0100
+++ b/QuotMain.thy	Mon Nov 02 18:26:55 2009 +0100
@@ -1,6 +1,7 @@
 theory QuotMain
 imports QuotScript QuotList Prove
-uses ("quotient.ML")
+uses ("quotient_info.ML") 
+     ("quotient.ML")
 begin
 
 ML {* Attrib.empty_binding *}
@@ -139,6 +140,7 @@
 
 section {* type definition for the quotient type *}
 
+use "quotient_info.ML"
 use "quotient.ML"
 
 declare [[map list = (map, LIST_REL)]]