--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Oct 21 19:13:09 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Oct 21 19:13:10 2010 +0200
@@ -255,7 +255,7 @@
let
val ctxt = ProofContext.init_global thy
fun is_nondefining_const (c, T) = member (op =) logic_operator_names c
- fun has_code_pred_intros (c, T) = can (Predicate_Compile_Core.intros_of ctxt) c
+ fun has_code_pred_intros (c, T) = can (Core_Data.intros_of ctxt) c
fun case_consts (c, T) = is_some (Datatype.info_of_case thy c)
fun is_datatype_constructor (c, T) = is_some (Datatype.info_of_constr thy (c, T))
fun defiants_of specs =