# HG changeset patch
# User bulwahn
# Date 1274286249 -7200
# Node ID 8da3b51726aca52f5e474b3e587632e6f11e6df5
# Parent  1166704995300fef5606f3ba9261f571e3dceed4
adapting examples

diff -r 116670499530 -r 8da3b51726ac src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Wed May 19 18:24:09 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Wed May 19 18:24:09 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 @{theory} @{const_name specialised_nth_el'P} *}
+ML {* Predicate_Compile_Core.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 @{theory} @{const_name specialised_max_natP} *}
+ML {* Predicate_Compile_Core.intros_of @{context} @{const_name specialised_max_natP} *}
 
 values "{x. max_of_my_SucP x 6}"