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