src/HOL/Tools/inductive.ML

--- a/src/HOL/Tools/inductive.ML	Fri Nov 07 20:43:13 2014 +0100
+++ b/src/HOL/Tools/inductive.ML	Fri Nov 07 22:15:51 2014 +0100
@@ -1007,9 +1007,6 @@
     cnames_syn pnames spec monos lthy =
   let
     val thy = Proof_Context.theory_of lthy;
-    val _ =
-      Theory.requires thy (Context.theory_name @{theory})
-        (coind_prefix coind ^ "inductive definitions");
 
 
     (* abbrevs *)