diff -r f7c00119e6e7 -r ca53150406c9 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Nov 14 18:37:49 2015 +0100
+++ b/src/HOL/Finite_Set.thy	Sun Nov 15 12:39:51 2015 +0100
@@ -11,11 +11,17 @@
 
 subsection \<open>Predicate for finite sets\<close>
 
+context
+  notes [[inductive_defs]]
+begin
+
 inductive finite :: "'a set \<Rightarrow> bool"
   where
     emptyI [simp, intro!]: "finite {}"
   | insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)"
 
+end
+
 simproc_setup finite_Collect ("finite (Collect P)") = \<open>K Set_Comprehension_Pointfree.simproc\<close>
 
 declare [[simproc del: finite_Collect]]