diff -r 2d7619fc0e1a -r 7fa9605b226c src/HOL/String.thy
--- a/src/HOL/String.thy	Tue Aug 18 21:45:24 2020 +0100
+++ b/src/HOL/String.thy	Wed Aug 19 12:58:28 2020 +0100
@@ -158,7 +158,7 @@
 proof -
   have "range (of_char :: char \<Rightarrow> nat) = of_char ` char_of ` {0::nat..<256}"
     by (auto simp add: range_nat_of_char intro!: image_eqI)
-  with inj_of_char [where ?'a = nat] show ?thesis 
+  with inj_of_char [where ?'a = nat] show ?thesis
     by (simp add: inj_image_eq_iff)
 qed
 
@@ -523,16 +523,16 @@
 begin
 
 qualified lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
-  is "order.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))"
+  is "ord.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))"
   .
 
 qualified lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
-  is "order.lexordp (\<lambda>c d. of_char c < (of_char d :: nat))"
+  is "ord.lexordp (\<lambda>c d. of_char c < (of_char d :: nat))"
   .
 
 instance proof -
-  from linorder_char interpret linorder "order.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))"
-    "order.lexordp (\<lambda>c d. of_char c < (of_char d :: nat)) :: string \<Rightarrow> string \<Rightarrow> bool"
+  from linorder_char interpret linorder "ord.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))"
+    "ord.lexordp (\<lambda>c d. of_char c < (of_char d :: nat)) :: string \<Rightarrow> string \<Rightarrow> bool"
     by (rule linorder.lexordp_linorder)
   show "PROP ?thesis"
     by (standard; transfer) (simp_all add: less_le_not_le linear)
@@ -602,7 +602,7 @@
   fix cs
   assume "\<forall>c\<in>set cs. \<not> digit7 c"
   then show "map (String.ascii_of \<circ> char_of) (map of_char cs) = cs"
-    by (induction cs) (simp_all add: String.ascii_of_idem) 
+    by (induction cs) (simp_all add: String.ascii_of_idem)
 qed
 
 qualified lemma explode_code [code]:
@@ -628,7 +628,7 @@
 text \<open>Alternative constructor for generated computations\<close>
 
 context
-begin  
+begin
 
 qualified definition Literal' :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> String.literal \<Rightarrow> String.literal"
   where [simp]: "Literal' = String.Literal"