src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
changeset 36998 116670499530
parent 36633 bafd82950e24
child 39034 37a9092de102
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Wed May 19 18:24:08 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Wed May 19 18:24:09 2010 +0200
     1.3 @@ -181,7 +181,7 @@
     1.4                      if member (op =) ((map fst specs) @ black_list) pred_name then
     1.5                        thy
     1.6                      else
     1.7 -                      (case try (Predicate_Compile_Core.intros_of thy) pred_name of
     1.8 +                      (case try (Predicate_Compile_Core.intros_of (ProofContext.init_global thy)) pred_name of
     1.9                          NONE => thy
    1.10                        | SOME [] => thy
    1.11                        | SOME intros =>