# HG changeset patch
# User bulwahn
# Date 1270046681 -7200
# Node ID c240b2a5df90eebbefd1a8508d75f90a34ee8b69
# Parent  8103572203886ef394cb403725dd2a18692f5412
no specialisation for predicates without introduction rules in the predicate compiler

diff -r 810357220388 -r c240b2a5df90 src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
--- 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)