diff -r e8d2ecf6aaac -r 9c8d63b4b6be src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
--- 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}"