# HG changeset patch
# User bulwahn
# Date 1268399099 -3600
# Node ID c029f85d3879ef8972baaf80c558c3dad499f746
# Parent  c2884bec546367a84893ee94a0cf89419609c666
adopting predicate compiler to changes in Spec_Rules; removed dependency to Nitpick_Intros

diff -r c2884bec5463 -r c029f85d3879 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Mar 12 12:14:31 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Mar 12 14:04:59 2010 +0100
@@ -198,15 +198,12 @@
           SOME th
         else
           NONE
-    val spec = case map_filter filtering (map (normalize thy o Thm.transfer thy) (Predicate_Compile_Alternative_Defs.get ctxt))
-     of [] => (case Spec_Rules.retrieve ctxt t
-       of [] => (case rev ( 
-         (map_filter filtering (map (normalize_intros thy o Thm.transfer thy)
-           (Nitpick_Intros.get ctxt))))
-         of [] => error ("No specification for " ^ (Syntax.string_of_term_global thy t))
-          | ths => ths)
-       | ((_, (_, ths)) :: _) => map (normalize_equation thy o Thm.transfer thy) ths)
-     | ths => rev ths
+    fun filter_defs ths = map_filter filtering (map (normalize thy o Thm.transfer thy) ths)
+    val spec = case filter_defs (Predicate_Compile_Alternative_Defs.get ctxt) of
+      [] => (case Spec_Rules.retrieve ctxt t of
+          [] => error ("No specification for " ^ (Syntax.string_of_term_global thy t))
+        | ((_, (_, ths)) :: _) => filter_defs ths)
+    | ths => rev ths
     val _ =
       if show_intermediate_results options then
         Output.tracing (commas (map (Display.string_of_thm_global thy) spec))