--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Sat Jan 05 17:24:33 2019 +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_val \<open>Core_Data.intros_of @{context} @{const_name specialised_nth_el'P}\<close>
+ML_val \<open>Core_Data.intros_of \<^context> \<^const_name>\<open>specialised_nth_el'P\<close>\<close>
thm greater_than_index.equation
@@ -44,7 +44,7 @@
thm max_of_my_SucP.equation
-ML_val \<open>Core_Data.intros_of @{context} @{const_name specialised_max_natP}\<close>
+ML_val \<open>Core_Data.intros_of \<^context> \<^const_name>\<open>specialised_max_natP\<close>\<close>
values "{x. max_of_my_SucP x 6}"