diff -r faeccede9534 -r 3c628937899d src/HOL/Tools/Predicate_Compile/core_data.ML
--- 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