--- 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)))
--- 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