use qualified names for rsp and rep_eq theorems in quotient_def

--- a/src/HOL/Library/Multiset.thy	Thu Mar 29 17:40:44 2012 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu Mar 29 21:13:48 2012 +0200
@@ -1186,7 +1186,7 @@
 
 lemma single_Bag [code]:
   "{#x#} = Bag (DAList.update x 1 DAList.empty)"
-  by (simp add: multiset_eq_iff alist.Alist_inverse update_code_eqn empty_code_eqn)
+  by (simp add: multiset_eq_iff alist.Alist_inverse update.rep_eq empty.rep_eq)
 
 lemma union_Bag [code]:
   "Bag xs + Bag ys = Bag (join (\<lambda>x (n1, n2). n1 + n2) xs ys)"
@@ -1199,7 +1199,7 @@
 
 lemma filter_Bag [code]:
   "Multiset.filter P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)"
-by (rule multiset_eqI) (simp add: count_of_filter filter_code_eqn)
+by (rule multiset_eqI) (simp add: count_of_filter filter.rep_eq)
 
 lemma mset_less_eq_Bag [code]:
   "Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)"

--- a/src/HOL/Quotient_Examples/FSet.thy	Thu Mar 29 17:40:44 2012 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy	Thu Mar 29 21:13:48 2012 +0200
@@ -1103,7 +1103,7 @@
       then have e': "List.member r a" using list_eq_def [simplified List.member_def [symmetric], of l r] b 
         by auto
       have f: "card_list (removeAll a l) = m" using e d by (simp)
-      have g: "removeAll a l \<approx> removeAll a r" using remove_fset_rsp b by simp
+      have g: "removeAll a l \<approx> removeAll a r" using remove_fset.rsp b by simp
       have "(removeAll a l) \<approx>2 (removeAll a r)" by (rule Suc.hyps[OF f g])
       then have h: "(a # removeAll a l) \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(5))
       have i: "l \<approx>2 (a # removeAll a l)"

--- a/src/HOL/Tools/Quotient/quotient_def.ML	Thu Mar 29 17:40:44 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Thu Mar 29 21:13:48 2012 +0200
@@ -189,9 +189,13 @@
 
     (* data storage *)
     val qconst_data = {qconst = trm, rconst = rhs, def = def_thm}
-    val lhs_name = #1 var
-    val rsp_thm_name = Binding.suffix_name "_rsp" lhs_name
-    val code_eqn_thm_name = Binding.suffix_name "_code_eqn" lhs_name
+     
+    fun qualify defname suffix = Binding.name suffix
+      |> Binding.qualify true defname
+
+    val lhs_name = Binding.name_of (#1 var)
+    val rsp_thm_name = qualify lhs_name "rsp"
+    val code_eqn_thm_name = qualify lhs_name "rep_eq"
     
     val lthy'' = lthy'
       |> Local_Theory.declaration {syntax = false, pervasive = true}