1.1 --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Wed May 19 18:24:09 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Wed May 19 18:24:09 2010 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4    "greater_than_index xs = (\<forall>i x. nth_el' xs i = Some x --> x > i)"
     1.5  
     1.6  code_pred (expected_modes: i => bool) [inductify, skip_proof, specialise] greater_than_index .
     1.7 -ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name specialised_nth_el'P} *}
     1.8 +ML {* Predicate_Compile_Core.intros_of @{context} @{const_name specialised_nth_el'P} *}
     1.9  
    1.10  thm greater_than_index.equation
    1.11  
    1.12 @@ -42,7 +42,7 @@
    1.13  
    1.14  thm max_of_my_SucP.equation
    1.15  
    1.16 -ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name specialised_max_natP} *}
    1.17 +ML {* Predicate_Compile_Core.intros_of @{context} @{const_name specialised_max_natP} *}
    1.18  
    1.19  values "{x. max_of_my_SucP x 6}"
    1.20