--- a/Quot/Examples/FSet3.thy	Sun Dec 27 23:33:10 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Wed Dec 30 12:10:57 2009 +0000
@@ -2,6 +2,16 @@
 imports "../QuotMain" "../QuotList" List
 begin
 
+ML {*
+structure QuotientRules = Named_Thms
+  (val name = "quot_thm"
+   val description = "Quotient theorems.")
+*}
+
+ML {*
+open QuotientRules
+*}
+
 fun
   list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
 where