src/HOL/Tools/inductive.ML

 fun gen_add_inductive_i mk_def
     (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono})
     cnames_syn pnames spec monos lthy =
   let
     val thy = Proof_Context.theory_of lthy;
-    val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
+    val _ =
+      Theory.requires thy (Context.theory_name @{theory})
+        (coind_prefix coind ^ "inductive definitions");
 
 
     (* abbrevs *)
 
     val (_, ctxt1) = Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn) lthy;