1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Jan 20 18:08:08 2010 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Jan 21 12:18:41 2010 +0100
     1.3 @@ -201,16 +201,10 @@
     1.4            NONE
     1.5    in
     1.6      case map_filter filtering (map (Thm.transfer thy) (Predicate_Compile_Alternative_Defs.get ctxt))
     1.7 -     of [] => (case map_filter
     1.8 -       (fn (roughly, (ts, ths)) =>
     1.9 -         if roughly = Spec_Rules.Equational andalso member (op =) ts t then SOME ths else NONE)
    1.10 -         (map ((apsnd o apsnd) (map (Thm.transfer thy))) (Spec_Rules.retrieve ctxt t))
    1.11 -       of [] => Output.cond_timeit true "Nitpick get_spec"
    1.12 -         (fn () => (case map_filter filtering (map (Thm.transfer thy) (Nitpick_Simps.get ctxt))
    1.13 -         of [] => map_filter filtering (map (Thm.transfer thy) (Nitpick_Intros.get ctxt))
    1.14 -         | ths => ths))
    1.15 -       | thss => flat thss)
    1.16 -     | ths => ths
    1.17 +     of [] => (case Spec_Rules.retrieve ctxt t
    1.18 +       of [] => rev (map_filter filtering (map (Thm.transfer thy) (Nitpick_Intros.get ctxt)))
    1.19 +       | ((_, (_, ths)) :: _) => map (normalize_equation thy o Thm.transfer thy) ths)
    1.20 +     | ths => rev ths
    1.21    end)
    1.22  
    1.23  val logic_operator_names =
    1.24 @@ -265,7 +259,7 @@
    1.25        |> filter is_defining_constname*)
    1.26      fun extend t =
    1.27        let
    1.28 -        val specs = rev (get_specification thy t)
    1.29 +        val specs = get_specification thy t
    1.30            |> map (inline_equations thy)
    1.31            (*|> Predicate_Compile_Set.unfold_set_notation*)
    1.32          (*val _ = print_specification options thy constname specs*)

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