diff -r e61e023c9faf -r 9701dbc35f86 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Feb 10 13:47:31 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Feb 10 14:33:47 2014 +0100
@@ -285,7 +285,7 @@
         |> Sign.add_consts_i
           (map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn))
            dst_preds)
-        |> fold_map Specification.axiom
+        |> fold_map Specification.axiom  (* FIXME !?!?!?! *)
             (map_index (fn (j, (predname, t)) =>
                 ((Binding.name (Long_Name.base_name predname ^ "_intro_" ^ string_of_int (j + 1)), []), t))
               (maps (uncurry (map o pair)) (prednames ~~ intr_tss)))