--- a/src/HOL/List.thy Thu Jan 07 15:50:09 2016 +0100
+++ b/src/HOL/List.thy Thu Jan 07 15:53:39 2016 +0100
@@ -5586,7 +5586,7 @@
begin
context
- notes [[inductive_defs]]
+ notes [[inductive_internals]]
begin
inductive lexordp :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"