src/HOL/List.thy

--- a/src/HOL/List.thy	Tue Aug 18 21:45:24 2020 +0100
+++ b/src/HOL/List.thy	Wed Aug 19 12:58:28 2020 +0100
@@ -6748,7 +6748,7 @@
   Author: Andreas Lochbihler
 \<close>
 
-context order
+context ord
 begin
 
 context
@@ -6812,8 +6812,8 @@
 
 end
 
-declare order.lexordp_simps [simp, code]
-declare order.lexordp_eq_simps [code, simp]
+declare ord.lexordp_simps [simp, code]
+declare ord.lexordp_eq_simps [code, simp]
 
 context order
 begin