use Item_Net to store inductive info

--- a/src/HOL/Library/Countable.thy	Wed Apr 05 22:29:09 2017 +0200
+++ b/src/HOL/Library/Countable.thy	Wed Apr 05 19:23:41 2017 +0200
@@ -176,7 +176,7 @@
           (case HOLogic.dest_Trueprop (Thm.concl_of typedef_thm) of
             (_ $ _ $ _ $ (_ $ Const (n, _))) => n
           | _ => raise Match)
-        val induct_info = Inductive.the_inductive ctxt pred_name
+        val induct_info = Inductive.the_inductive_global ctxt pred_name
         val pred_names = #names (fst induct_info)
         val induct_thms = #inducts (snd induct_info)
         val alist = pred_names ~~ induct_thms

--- a/src/HOL/Nominal/nominal_inductive.ML	Wed Apr 05 22:29:09 2017 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Apr 05 19:23:41 2017 +0200
@@ -150,7 +150,7 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     val ({names, ...}, {raw_induct, intrs, elims, ...}) =
-      Inductive.the_inductive ctxt (Sign.intern_const thy s);
+      Inductive.the_inductive_global ctxt (Sign.intern_const thy s);
     val ind_params = Inductive.params_of raw_induct;
     val raw_induct = atomize_induct ctxt raw_induct;
     val elims = map (atomize_induct ctxt) elims;
@@ -591,7 +591,7 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     val ({names, ...}, {raw_induct, intrs, elims, ...}) =
-      Inductive.the_inductive ctxt (Sign.intern_const thy s);
+      Inductive.the_inductive_global ctxt (Sign.intern_const thy s);
     val raw_induct = atomize_induct ctxt raw_induct;
     val elims = map (atomize_induct ctxt) elims;
     val intrs = map (atomize_intr ctxt) intrs;

--- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Apr 05 22:29:09 2017 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Apr 05 19:23:41 2017 +0200
@@ -155,7 +155,7 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     val ({names, ...}, {raw_induct, intrs, elims, ...}) =
-      Inductive.the_inductive ctxt (Sign.intern_const thy s);
+      Inductive.the_inductive_global ctxt (Sign.intern_const thy s);
     val ind_params = Inductive.params_of raw_induct;
     val raw_induct = atomize_induct ctxt raw_induct;
     val elims = map (atomize_induct ctxt) elims;

--- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Wed Apr 05 22:29:09 2017 +0200
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Wed Apr 05 19:23:41 2017 +0200
@@ -265,7 +265,7 @@
 val no_compilation = ([], ([], []))
 
 fun fetch_pred_data ctxt name =
-  (case try (Inductive.the_inductive ctxt) name of
+  (case try (Inductive.the_inductive_global ctxt) name of
     SOME (info as (_, result)) =>
       let
         val thy = Proof_Context.theory_of ctxt
@@ -293,7 +293,7 @@
   in PredData.map (Graph.map_node name (map_pred_data add)) end
 
 fun is_inductive_predicate ctxt name =
-  is_some (try (Inductive.the_inductive ctxt) name)
+  is_some (try (Inductive.the_inductive_global ctxt) name)
 
 fun depending_preds_of ctxt (key, value) =
   let

--- a/src/HOL/Tools/inductive.ML	Wed Apr 05 22:29:09 2017 +0200
+++ b/src/HOL/Tools/inductive.ML	Wed Apr 05 19:23:41 2017 +0200
@@ -25,7 +25,8 @@
      induct: thm, inducts: thm list, intrs: thm list, eqs: thm list}
   val transform_result: morphism -> inductive_result -> inductive_result
   type inductive_info = {names: string list, coind: bool} * inductive_result
-  val the_inductive: Proof.context -> string -> inductive_info
+  val the_inductive: Proof.context -> term -> inductive_info
+  val the_inductive_global: Proof.context -> string -> inductive_info
   val print_inductives: bool -> Proof.context -> unit
   val get_monos: Proof.context -> thm list
   val mono_add: attribute
@@ -202,12 +203,15 @@
 
 type inductive_info = {names: string list, coind: bool} * inductive_result;
 
+val empty_infos =
+  Item_Net.init (op = o apply2 (#names o fst)) (#preds o snd)
+
 val empty_equations =
   Item_Net.init Thm.eq_thm_prop
     (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of);
 
 datatype data = Data of
- {infos: inductive_info Symtab.table,
+ {infos: inductive_info Item_Net.T,
   monos: thm list,
   equations: thm Item_Net.T};
 
@@ -217,11 +221,11 @@
 structure Data = Generic_Data
 (
   type T = data;
-  val empty = make_data (Symtab.empty, [], empty_equations);
+  val empty = make_data (empty_infos, [], empty_equations);
   val extend = I;
   fun merge (Data {infos = infos1, monos = monos1, equations = equations1},
       Data {infos = infos2, monos = monos2, equations = equations2}) =
-    make_data (Symtab.merge (K true) (infos1, infos2),
+    make_data (Item_Net.merge (infos1, infos2),
       Thm.merge_thms (monos1, monos2),
       Item_Net.merge (equations1, equations2));
 );
@@ -235,26 +239,34 @@
   let
     val {infos, monos, ...} = rep_data ctxt;
     val space = Consts.space_of (Proof_Context.consts_of ctxt);
+    val consts =
+      Item_Net.content infos
+      |> maps (fn ({names, ...}, result) => map (rpair result) names)
   in
     [Pretty.block
       (Pretty.breaks
         (Pretty.str "(co)inductives:" ::
           map (Pretty.mark_str o #1)
-            (Name_Space.markup_entries verbose ctxt space (Symtab.dest infos)))),
+            (Name_Space.markup_entries verbose ctxt space consts))),
      Pretty.big_list "monotonicity rules:" (map (Thm.pretty_thm_item ctxt) monos)]
   end |> Pretty.writeln_chunks;
 
 
 (* inductive info *)
 
-fun the_inductive ctxt name =
-  (case Symtab.lookup (#infos (rep_data ctxt)) name of
-    NONE => error ("Unknown (co)inductive predicate " ^ quote name)
-  | SOME info => info);
+fun the_inductive ctxt term =
+  Item_Net.retrieve (#infos (rep_data ctxt)) term
+  |> the_single
 
-fun put_inductives names info =
+fun the_inductive_global ctxt name =
+  #infos (rep_data ctxt)
+  |> Item_Net.content
+  |> filter (fn ({names, ...}, _) => member op = names name)
+  |> the_single
+
+fun put_inductives info =
   map_data (fn (infos, monos, equations) =>
-    (fold (fn name => Symtab.update (name, info)) names infos, monos, equations));
+    (Item_Net.update info infos, monos, equations));
 
 
 (* monotonicity rules *)
@@ -1133,7 +1145,7 @@
     val lthy4 = lthy3
       |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi =>
         let val result' = transform_result phi result;
-        in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end);
+        in put_inductives ({names = cnames, coind = coind}, result') end);
   in (result, lthy4) end;
 
 
@@ -1218,7 +1230,7 @@
       |> Named_Target.theory_init
       |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
       |> Local_Theory.exit;
-    val info = #2 (the_inductive ctxt' name);
+    val info = #2 (the_inductive_global ctxt' name);
   in (info, Proof_Context.theory_of ctxt') end;
 
 

--- a/src/HOL/Tools/inductive_realizer.ML	Wed Apr 05 22:29:09 2017 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Wed Apr 05 19:23:41 2017 +0200
@@ -149,7 +149,7 @@
       | is_meta (Const (@{const_name Pure.imp}, _) $ _ $ Q) = is_meta Q
       | is_meta (Const (@{const_name Trueprop}, _) $ t) =
           (case head_of t of
-            Const (s, _) => can (Inductive.the_inductive ctxt) s
+            Const (s, _) => can (Inductive.the_inductive_global ctxt) s
           | _ => true)
       | is_meta _ = false;
 
@@ -493,7 +493,7 @@
 fun add_ind_realizers name rsets thy =
   let
     val (_, {intrs, induct, raw_induct, elims, ...}) =
-      Inductive.the_inductive (Proof_Context.init_global thy) name;
+      Inductive.the_inductive_global (Proof_Context.init_global thy) name;
     val vss = sort (int_ord o apply2 length)
       (subsets (map fst (relevant_vars (Thm.concl_of (hd intrs)))))
   in