diff -r 9ace5f5bae69 -r bd73a2279fcd src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Jan 07 15:50:09 2016 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Jan 07 15:53:39 2016 +0100
@@ -12,7 +12,7 @@
 subsection \<open>Predicate for finite sets\<close>
 
 context
-  notes [[inductive_defs]]
+  notes [[inductive_internals]]
 begin
 
 inductive finite :: "'a set \<Rightarrow> bool"