src/HOL/Library/Multiset_Permutations.thy

   unfolding permutations_of_multiset_def by simp
 
 lemma permutations_of_multiset_nonempty: 
   assumes nonempty: "A \<noteq> {#}"
   shows   "permutations_of_multiset A = 
-             (\<Union>x\<in>set_mset A. (op # x) ` permutations_of_multiset (A - {#x#}))" (is "_ = ?rhs")
+             (\<Union>x\<in>set_mset A. ((#) x) ` permutations_of_multiset (A - {#x#}))" (is "_ = ?rhs")
 proof safe
   fix xs assume "xs \<in> permutations_of_multiset A"
   hence mset_xs: "mset xs = A" by (simp add: permutations_of_multiset_def)
   hence "xs \<noteq> []" by (auto simp: nonempty)
   then obtain x xs' where xs: "xs = x # xs'" by (cases xs) simp_all

 lemma card_permutations_of_multiset_aux:
   "card (permutations_of_multiset A) * (\<Prod>x\<in>set_mset A. fact (count A x)) = fact (size A)"
 proof (induction A rule: multiset_remove_induct)
   case (remove A)
   have "card (permutations_of_multiset A) = 
-          card (\<Union>x\<in>set_mset A. op # x ` permutations_of_multiset (A - {#x#}))"
+          card (\<Union>x\<in>set_mset A. (#) x ` permutations_of_multiset (A - {#x#}))"
     by (simp add: permutations_of_multiset_nonempty remove.hyps)
   also have "\<dots> = (\<Sum>x\<in>set_mset A. card (permutations_of_multiset (A - {#x#})))"
     by (subst card_UN_disjoint) (auto simp: card_image)
   also have "\<dots> * (\<Prod>x\<in>set_mset A. fact (count A x)) = 
                (\<Sum>x\<in>set_mset A. card (permutations_of_multiset (A - {#x#})) * 

 
 declare length_remove1 [termination_simp] 
 
 fun permutations_of_list_impl where
   "permutations_of_list_impl xs = (if xs = [] then [[]] else
-     List.bind (remdups xs) (\<lambda>x. map (op # x) (permutations_of_list_impl (remove1 x xs))))"
+     List.bind (remdups xs) (\<lambda>x. map ((#) x) (permutations_of_list_impl (remove1 x xs))))"
 
 fun permutations_of_list_impl_aux where
   "permutations_of_list_impl_aux acc xs = (if xs = [] then [acc] else
      List.bind (remdups xs) (\<lambda>x. permutations_of_list_impl_aux (x#acc) (remove1 x xs)))"
 

   "permutations_of_list_impl [] = [[]]"
   by (simp add: permutations_of_list_impl.simps)
 
 lemma permutations_of_list_impl_nonempty:
   "xs \<noteq> [] \<Longrightarrow> permutations_of_list_impl xs = 
-     List.bind (remdups xs) (\<lambda>x. map (op # x) (permutations_of_list_impl (remove1 x xs)))"
+     List.bind (remdups xs) (\<lambda>x. map ((#) x) (permutations_of_list_impl (remove1 x xs)))"
   by (subst permutations_of_list_impl.simps) simp_all
 
 lemma set_permutations_of_list_impl:
   "set (permutations_of_list_impl xs) = permutations_of_multiset (mset xs)"
   by (induction xs rule: permutations_of_list_impl.induct)