diff -r 070161f1996a -r a082e2d138ab quotient.ML
--- a/quotient.ML	Sun Dec 06 11:39:34 2009 +0100
+++ b/quotient.ML	Sun Dec 06 13:41:42 2009 +0100
@@ -28,6 +28,8 @@
   (thm', lthy')
 end
 
+fun internal_attr at = Attrib.internal (K at)
+
 fun theorem after_qed goals ctxt =
 let
   val goals' = map (rpair []) goals
@@ -157,7 +159,8 @@
   (* FIXME: to recalculated in for example REGULARIZE *)
 
   (* storing of the equiv_thm under a name *)
-  val (_, lthy4) = note (Binding.suffix_name "_equivp" qty_name, equiv_thm, []) lthy3
+  val (_, lthy4) = note (Binding.suffix_name "_equivp" qty_name, equiv_thm, 
+                           [internal_attr equiv_rules_add]) lthy3
 
   (* interpretation *)
   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
@@ -179,7 +182,7 @@
 in
   lthy6
   |> note (quot_thm_name, quot_thm, [])
-  ||>> note (quotient_thm_name, quotient_thm, [Attrib.internal (K quotient_rules_add)])
+  ||>> note (quotient_thm_name, quotient_thm, [internal_attr quotient_rules_add])
   ||> Local_Theory.theory (fn thy =>
       let
         val global_eqns = map exp_term [eqn2i, eqn1i];