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