# HG changeset patch
# User wenzelm
# Date 1362072931 -3600
# Node ID 0e70cc4e94e8270f267caaad36354aea2bf48a9c
# Parent  dfe469293eb4f827cea694a28b781fb9d19eb2c4
provide explicit dummy names (cf. dfe469293eb4);

diff -r dfe469293eb4 -r 0e70cc4e94e8 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- 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