--- 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 =