--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Feb 28 17:38:35 2013 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Feb 28 18:35:31 2013 +0100
@@ -285,7 +285,8 @@
|> Sign.add_consts_i
(map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn))
dst_preds)
- |> fold_map Specification.axiom (map (pair (Binding.empty, [])) intr_ts)
+ |> fold_map Specification.axiom
+ (map (fn t => ((Binding.name ("unnamed_axiom_" ^ serial_string ()), []), t)) intr_ts)
val specs = map (fn predname => (predname,
map Drule.export_without_context (filter (Predicate_Compile_Aux.is_intro predname) intrs)))
dst_prednames