src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy

 
 definition
   "greater_than_index xs = (\<forall>i x. nth_el' xs i = Some x --> x > i)"
 
 code_pred (expected_modes: i => bool) [inductify, skip_proof, specialise] greater_than_index .
-ML {* Predicate_Compile_Core.intros_of @{context} @{const_name specialised_nth_el'P} *}
+ML {* Core_Data.intros_of @{context} @{const_name specialised_nth_el'P} *}
 
 thm greater_than_index.equation
 
 values [expected "{()}"] "{x. greater_than_index [1,2,4,6]}"
 values [expected "{}"] "{x. greater_than_index [0,2,3,2]}"

 
 code_pred (modes: o => i => bool) [inductify, specialise, skip_proof] max_of_my_Suc .
 
 thm max_of_my_SucP.equation
 
-ML {* Predicate_Compile_Core.intros_of @{context} @{const_name specialised_max_natP} *}
+ML {* Core_Data.intros_of @{context} @{const_name specialised_max_natP} *}
 
 values "{x. max_of_my_SucP x 6}"
 
 subsection {* Sorts *}