Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
provide explicit dummy names (cf. dfe469293eb4);
authorwenzelm
Thu, 28 Feb 2013 18:35:31 +0100
changeset 51317 0e70cc4e94e8
parent 51316 dfe469293eb4
child 51318 e6524a89c9e3
provide explicit dummy names (cf. dfe469293eb4);
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle