--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Thu Oct 21 19:13:10 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Thu Oct 21 19:13:11 2010 +0200
@@ -13,7 +13,7 @@
"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
@@ -42,7 +42,7 @@
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}"