no specialisation for predicates without introduction rules in the predicate compiler
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Wed Mar 31 16:44:41 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Wed Mar 31 16:44:41 2010 +0200
@@ -181,6 +181,7 @@
else
(case try (Predicate_Compile_Core.intros_of thy) pred_name of
NONE => thy
+ | SOME [] => thy
| SOME intros =>
specialise_intros ((map fst specs) @ (pred_name :: black_list))
(pred, intros) pats thy)