1.1 --- a/src/HOL/Library/Multiset.thy	Thu Mar 29 17:40:44 2012 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Thu Mar 29 21:13:48 2012 +0200
     1.3 @@ -1186,7 +1186,7 @@
     1.4  
     1.5  lemma single_Bag [code]:
     1.6    "{#x#} = Bag (DAList.update x 1 DAList.empty)"
     1.7 -  by (simp add: multiset_eq_iff alist.Alist_inverse update_code_eqn empty_code_eqn)
     1.8 +  by (simp add: multiset_eq_iff alist.Alist_inverse update.rep_eq empty.rep_eq)
     1.9  
    1.10  lemma union_Bag [code]:
    1.11    "Bag xs + Bag ys = Bag (join (\<lambda>x (n1, n2). n1 + n2) xs ys)"
    1.12 @@ -1199,7 +1199,7 @@
    1.13  
    1.14  lemma filter_Bag [code]:
    1.15    "Multiset.filter P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)"
    1.16 -by (rule multiset_eqI) (simp add: count_of_filter filter_code_eqn)
    1.17 +by (rule multiset_eqI) (simp add: count_of_filter filter.rep_eq)
    1.18  
    1.19  lemma mset_less_eq_Bag [code]:
    1.20    "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)"

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

     3.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Thu Mar 29 17:40:44 2012 +0200
     3.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Thu Mar 29 21:13:48 2012 +0200
     3.3 @@ -189,9 +189,13 @@
     3.4  
     3.5      (* data storage *)
     3.6      val qconst_data = {qconst = trm, rconst = rhs, def = def_thm}
     3.7 -    val lhs_name = #1 var
     3.8 -    val rsp_thm_name = Binding.suffix_name "_rsp" lhs_name
     3.9 -    val code_eqn_thm_name = Binding.suffix_name "_code_eqn" lhs_name
    3.10 +     
    3.11 +    fun qualify defname suffix = Binding.name suffix
    3.12 +      |> Binding.qualify true defname
    3.13 +
    3.14 +    val lhs_name = Binding.name_of (#1 var)
    3.15 +    val rsp_thm_name = qualify lhs_name "rsp"
    3.16 +    val code_eqn_thm_name = qualify lhs_name "rep_eq"
    3.17      
    3.18      val lthy'' = lthy'
    3.19        |> Local_Theory.declaration {syntax = false, pervasive = true}