diff -r 74d673b7d40e -r 3bfa28b3a5b2 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Thu Feb 21 09:15:06 2019 +0000
+++ b/src/HOL/Tools/inductive.ML	Thu Feb 21 09:15:07 2019 +0000
@@ -52,10 +52,6 @@
     flags -> ((binding * typ) * mixfix) list ->
     (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
     result * local_theory
-  val add_inductive_global:
-    flags -> ((binding * typ) * mixfix) list ->
-    (string * typ) list -> (Attrib.binding * term) list -> thm list -> theory ->
-    result * theory
   val add_inductive_cmd: bool -> bool ->
     (binding * string option * mixfix) list ->
     (binding * string option * mixfix) list ->
@@ -1226,16 +1222,6 @@
 val add_inductive = gen_add_inductive add_ind_def;
 val add_inductive_cmd = gen_add_inductive_cmd add_ind_def;
 
-fun add_inductive_global flags cnames_syn pnames pre_intros monos thy =
-  let
-    val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
-    val ctxt' = thy
-      |> Named_Target.theory_init
-      |> add_inductive flags cnames_syn pnames pre_intros monos |> snd
-      |> Local_Theory.exit;
-    val info = #2 (the_inductive_global ctxt' name);
-  in (info, Proof_Context.theory_of ctxt') end;
-
 
 (* read off arities of inductive predicates from raw induction rule *)
 fun arities_of induct =