--- a/QuotMain.thy	Tue Oct 27 11:43:02 2009 +0100
+++ b/QuotMain.thy	Tue Oct 27 14:14:30 2009 +0100
@@ -137,6 +137,8 @@
 
 section {* type definition for the quotient type *}
 
+ML {* Proof.theorem_i NONE *}
+
 use "quotient.ML"
 
 declare [[map list = (map, LIST_REL)]]