--- a/quotient.ML	Thu Dec 03 11:40:10 2009 +0100
+++ b/quotient.ML	Thu Dec 03 13:59:53 2009 +0100
@@ -5,7 +5,6 @@
   val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
   val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
 
-  val note: binding * thm -> local_theory -> thm * local_theory
 end;
 
 structure Quotient: QUOTIENT =
@@ -22,9 +21,9 @@
   ((rhs, thm), lthy')
 end
 
-fun note (name, thm) lthy =
+fun note (name, thm, attrs) lthy =
 let
-  val ((_,[thm']), lthy') = Local_Theory.note ((name, []), [thm]) lthy
+  val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy
 in
   (thm', lthy')
 end
@@ -158,7 +157,7 @@
   (* FIXME: to recalculated in for example REGULARIZE *)
 
   (* storing of the equiv_thm under a name *)
-  val (_, lthy4) = note (Binding.suffix_name "_equiv" qty_name, equiv_thm) lthy3
+  val (_, lthy4) = note (Binding.suffix_name "_equiv" qty_name, equiv_thm, []) lthy3
 
   (* interpretation *)
   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
@@ -179,8 +178,8 @@
     Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))]
 in
   lthy6
-  |> note (quot_thm_name, quot_thm)
-  ||>> note (quotient_thm_name, quotient_thm)
+  |> note (quot_thm_name, quot_thm, [])
+  ||>> note (quotient_thm_name, quotient_thm, [Attrib.internal (K quotient_rules_add)])
   ||> Local_Theory.theory (fn thy =>
       let
         val global_eqns = map exp_term [eqn2i, eqn1i];