1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed May 19 18:24:08 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed May 19 18:24:09 2010 +0200
     1.3 @@ -253,8 +253,9 @@
     1.4  
     1.5  fun obtain_specification_graph options thy t =
     1.6    let
     1.7 +    val ctxt = ProofContext.init_global thy
     1.8      fun is_nondefining_const (c, T) = member (op =) logic_operator_names c
     1.9 -    fun has_code_pred_intros (c, T) = can (Predicate_Compile_Core.intros_of thy) c
    1.10 +    fun has_code_pred_intros (c, T) = can (Predicate_Compile_Core.intros_of ctxt) c
    1.11      fun case_consts (c, T) = is_some (Datatype.info_of_case thy c)
    1.12      fun is_datatype_constructor (c, T) = is_some (Datatype.info_of_constr thy (c, T))
    1.13      fun defiants_of specs =