provide explicit dummy names (cf. dfe469293eb4);
authorwenzelm
Thu Feb 28 18:35:31 2013 +0100 (2013-02-28)
changeset 513170e70cc4e94e8
parent 51316 dfe469293eb4
child 51318 e6524a89c9e3
provide explicit dummy names (cf. dfe469293eb4);
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Feb 28 17:38:35 2013 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Feb 28 18:35:31 2013 +0100
     1.3 @@ -285,7 +285,8 @@
     1.4          |> Sign.add_consts_i
     1.5            (map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn))
     1.6             dst_preds)
     1.7 -        |> fold_map Specification.axiom (map (pair (Binding.empty, [])) intr_ts)
     1.8 +        |> fold_map Specification.axiom
     1.9 +            (map (fn t => ((Binding.name ("unnamed_axiom_" ^ serial_string ()), []), t)) intr_ts)
    1.10        val specs = map (fn predname => (predname,
    1.11            map Drule.export_without_context (filter (Predicate_Compile_Aux.is_intro predname) intrs)))
    1.12          dst_prednames