# HG changeset patch
# User cu@localhost
# Date 1262175057 0
# Node ID a422a51bb0ebda256895090537cb7671ac0c43f3
# Parent  35436401f00d827050b9fa5906644943fa2b6973
some small changes

diff -r 35436401f00d -r a422a51bb0eb Quot/Examples/FSet3.thy
--- 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
diff -r 35436401f00d -r a422a51bb0eb Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Sun Dec 27 23:33:10 2009 +0100
+++ b/Quot/quotient_info.ML	Wed Dec 30 12:10:57 2009 +0000
@@ -32,16 +32,15 @@
   val quotient_rules_add: attribute
 end;
 
-functor Named_Thms_Ext (val name: string val description: string val filter: thm -> thm): NAMED_THMS =
+
+functor Filtered_Named_Thms (val name: string val description: string val filter: thm -> thm): NAMED_THMS =
 struct
 
 structure Data = Generic_Data
-(
-  type T = thm Item_Net.T;
+( type T = thm Item_Net.T;
   val empty = Thm.full_rules;
   val extend = I;
-  val merge = Item_Net.merge;
-);
+  val merge = Item_Net.merge);
 
 val content = Item_Net.content o Data.get;
 val get = content o Context.Proof;
@@ -244,10 +243,10 @@
 val equiv_rules_add = EquivRules.add
 
 (* respectfulness theorems *)
-structure RspRules = Named_Thms_Ext
+structure RspRules = Filtered_Named_Thms
   (val name = "quot_respect"
    val description = "Respectfulness theorems."
-   val filter = fn x => x)
+   val filter = I)
 
 val rsp_rules_get = RspRules.get
 
@@ -282,7 +281,6 @@
      IdSimps.setup #>
      QuotientRules.setup))
 
-
 (* setup of the printing commands *)
 
 fun improper_command (pp_fn, cmd_name, descr_str) =