--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Mon Feb 25 12:17:11 2013 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Mon Feb 25 12:17:50 2013 +0100
@@ -15,7 +15,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 {* Core_Data.intros_of @{context} @{const_name specialised_nth_el'P} *}
+ML_val {* Core_Data.intros_of @{context} @{const_name specialised_nth_el'P} *}
thm greater_than_index.equation
@@ -44,7 +44,7 @@
thm max_of_my_SucP.equation
-ML {* Core_Data.intros_of @{context} @{const_name specialised_max_natP} *}
+ML_val {* Core_Data.intros_of @{context} @{const_name specialised_max_natP} *}
values "{x. max_of_my_SucP x 6}"