1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Oct 31 11:44:20 2013 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Oct 31 16:54:22 2013 +0100
     1.3 @@ -286,7 +286,9 @@
     1.4            (map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn))
     1.5             dst_preds)
     1.6          |> fold_map Specification.axiom
     1.7 -            (map (fn t => ((Binding.name ("unnamed_axiom_" ^ serial_string ()), []), t)) intr_ts)
     1.8 +            (map_index (fn (j, (predname, t)) =>
     1.9 +                ((Binding.name (Long_Name.base_name predname ^ "_intro_" ^ string_of_int (j + 1)), []), t))
    1.10 +              (prednames ~~ intr_ts))
    1.11        val specs = map (fn predname => (predname,
    1.12            map Drule.export_without_context (filter (Predicate_Compile_Aux.is_intro predname) intrs)))
    1.13          dst_prednames