adopting predicate compiler to new Spec_Rules and eliminating the use of Nitpick_Simps

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Jan 20 18:08:08 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Jan 21 12:18:41 2010 +0100
@@ -201,16 +201,10 @@
           NONE
   in
     case map_filter filtering (map (Thm.transfer thy) (Predicate_Compile_Alternative_Defs.get ctxt))
-     of [] => (case map_filter
-       (fn (roughly, (ts, ths)) =>
-         if roughly = Spec_Rules.Equational andalso member (op =) ts t then SOME ths else NONE)
-         (map ((apsnd o apsnd) (map (Thm.transfer thy))) (Spec_Rules.retrieve ctxt t))
-       of [] => Output.cond_timeit true "Nitpick get_spec"
-         (fn () => (case map_filter filtering (map (Thm.transfer thy) (Nitpick_Simps.get ctxt))
-         of [] => map_filter filtering (map (Thm.transfer thy) (Nitpick_Intros.get ctxt))
-         | ths => ths))
-       | thss => flat thss)
-     | ths => ths
+     of [] => (case Spec_Rules.retrieve ctxt t
+       of [] => rev (map_filter filtering (map (Thm.transfer thy) (Nitpick_Intros.get ctxt)))
+       | ((_, (_, ths)) :: _) => map (normalize_equation thy o Thm.transfer thy) ths)
+     | ths => rev ths
   end)
 
 val logic_operator_names =
@@ -265,7 +259,7 @@
       |> filter is_defining_constname*)
     fun extend t =
       let
-        val specs = rev (get_specification thy t)
+        val specs = get_specification thy t
           |> map (inline_equations thy)
           (*|> Predicate_Compile_Set.unfold_set_notation*)
         (*val _ = print_specification options thy constname specs*)

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Jan 20 18:08:08 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Jan 21 12:18:41 2010 +0100
@@ -340,7 +340,8 @@
             val prednames = map (fst o dest_Const) (#preds ind_result)
             (* val rewr_thms = map mk_rewr_eq ((distinct (op =) funs) ~~ (#preds ind_result)) *)
             (* add constants to my table *)
-            val specs = map (fn predname => (predname, filter (Predicate_Compile_Aux.is_intro predname) (#intrs ind_result))) prednames
+            val specs = map (fn predname => (predname, filter (Predicate_Compile_Aux.is_intro predname)
+              (#intrs ind_result))) prednames
             val thy'' = Pred_Compile_Preproc.map (fold Symtab.update_new (consts ~~ prednames)) thy'
           in
             (specs, thy'')