# HG changeset patch
# User wenzelm
# Date 1392039227 -3600
# Node ID 9701dbc35f867ba2ecbc49bd44758d5d1800f22a
# Parent  e61e023c9fafaa92b16a2dcbe87b50a12e492b9b
comments;

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)))
diff -r e61e023c9faf -r 9701dbc35f86 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Feb 10 13:47:31 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Feb 10 14:33:47 2014 +0100
@@ -118,8 +118,9 @@
           val new_defs = map mk_def srs
           val (definition, thy') = thy
           |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
-          |> fold_map Specification.axiom (map_index
-              (fn (i, t) => ((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs)
+          |> fold_map Specification.axiom  (* FIXME !?!?!?! *)
+            (map_index (fn (i, t) =>
+              ((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs)
         in
           (lhs, ((full_constname, map Drule.export_without_context definition) :: defs, thy'))
         end