# HG changeset patch
# User wenzelm
# Date 1536418538 -7200
# Node ID 53f7b6b9f73422750166af6a96c0d5e3fc0b5367
# Parent  25b431feb2e9df0eaae67c34d14caa1f43ae9cc3# Parent  e848328cb2c11c19211669944e29611efdc89074
merged

diff -r e848328cb2c1 -r 53f7b6b9f734 NEWS
--- a/NEWS	Sat Sep 08 16:52:38 2018 +0200
+++ b/NEWS	Sat Sep 08 16:55:38 2018 +0200
@@ -31,6 +31,10 @@
 * Sledgehammer: The URL for SystemOnTPTP, which is used by remote
 provers, has been updated.
 
+* Facts sum_mset.commute and prod_mset.commute renamed to sum_mset.swap
+and prod_mset.swap, similarly to sum.swap and prod.swap.
+INCOMPATIBILITY.
+
 
 *** ML ***
 
diff -r e848328cb2c1 -r 53f7b6b9f734 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Sep 08 16:52:38 2018 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat Sep 08 16:55:38 2018 +0200
@@ -2251,7 +2251,7 @@
     F (image_mset (g x) B) \<^bold>* F {#F {#g i j. i \<in># A#}. j \<in># B#}"
   by (induction B) (simp_all add: left_commute semigroup.assoc semigroup_axioms)
 
-lemma commute:
+lemma swap:
   "F (image_mset (\<lambda>i. F (image_mset (g i) B)) A) =
     F (image_mset (\<lambda>j. F (image_mset (\<lambda>i. g i j) A)) B)"
   apply (induction A, simp)
@@ -2348,7 +2348,7 @@
 lemma sum_mset_product:
   fixes f :: "'a::{comm_monoid_add,times} \<Rightarrow> 'b::semiring_0"
   shows "(\<Sum>i \<in># A. f i) * (\<Sum>i \<in># B. g i) = (\<Sum>i\<in>#A. \<Sum>j\<in>#B. f i * g j)"
-  by (subst sum_mset.commute) (simp add: sum_mset_distrib_left sum_mset_distrib_right)
+  by (subst sum_mset.swap) (simp add: sum_mset_distrib_left sum_mset_distrib_right)
 
 context semiring_1
 begin
diff -r e848328cb2c1 -r 53f7b6b9f734 src/HOL/Tools/literal.ML
--- a/src/HOL/Tools/literal.ML	Sat Sep 08 16:52:38 2018 +0200
+++ b/src/HOL/Tools/literal.ML	Sat Sep 08 16:55:38 2018 +0200
@@ -36,7 +36,7 @@
 fun literal_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
       c $ literal_tr [t] $ u
   | literal_tr [Free (str, _)] =
-      (mk_literal_syntax o map ord o String_Syntax.plain_strings_of) str
+      (mk_literal_syntax o map String_Syntax.ascii_ord_of o String_Syntax.plain_strings_of) str
   | literal_tr ts = raise TERM ("literal_tr", ts);
 
 fun ascii k = Syntax.const @{syntax_const "_Ascii"}
diff -r e848328cb2c1 -r 53f7b6b9f734 src/HOL/Tools/string_syntax.ML
--- a/src/HOL/Tools/string_syntax.ML	Sat Sep 08 16:52:38 2018 +0200
+++ b/src/HOL/Tools/string_syntax.ML	Sat Sep 08 16:55:38 2018 +0200
@@ -8,6 +8,7 @@
   val hex: int -> string
   val mk_bits_syntax: int -> int -> term list
   val dest_bits_syntax: term list -> int
+  val ascii_ord_of: string -> int
   val plain_strings_of: string -> string list
   datatype character = Char of string | Ord of int
   val classify_character: int -> character
@@ -47,14 +48,14 @@
 
 (* char *)
 
+fun ascii_ord_of c =
+  if Symbol.is_ascii c then ord c
+  else if c = "\<newline>" then 10
+  else error ("Bad character: " ^ quote c);
+
 fun mk_char_syntax i =
   list_comb (Syntax.const @{const_syntax Char}, mk_bits_syntax 8 i);
 
-fun mk_char_syntax' c =
-  if Symbol.is_ascii c then mk_char_syntax (ord c)
-  else if c = "\<newline>" then mk_char_syntax 10
-  else error ("Bad character: " ^ quote c);
-
 fun plain_strings_of str =
   map fst (Lexicon.explode_str (str, Position.none));
 
@@ -84,7 +85,7 @@
       c $ char_tr [t] $ u
   | char_tr [Free (str, _)] =
       (case plain_strings_of str of
-        [c] => mk_char_syntax' c
+        [c] => mk_char_syntax (ascii_ord_of c)
       | _ => error ("Single character expected: " ^ str))
   | char_tr ts = raise TERM ("char_tr", ts);
 
@@ -107,7 +108,8 @@
 
 fun mk_string_syntax [] = Syntax.const @{const_syntax Nil}
   | mk_string_syntax (c :: cs) =
-      Syntax.const @{const_syntax Cons} $ mk_char_syntax' c $ mk_string_syntax cs;
+      Syntax.const @{const_syntax Cons} $ mk_char_syntax (ascii_ord_of c)
+        $ mk_string_syntax cs;
 
 fun mk_string_ast ss =
   Ast.Appl [Ast.Constant @{syntax_const "_inner_string"},