Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/specification.ML
changeset 42375 774df7c59508
parent 42360 da8817d01e7c
child 42440 5e7a7343ab11 
--- a/src/Pure/Isar/specification.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/Isar/specification.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -180,7 +180,7 @@
 
     (*axioms*)
     val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
-        fold_map Thm.add_axiom
+        fold_map Thm.add_axiom_global
           (map (apfst (fn a => Binding.map_name (K a) b))
             (Global_Theory.name_multi (Variable.name b) (map subst props)))
         #>> (fn ths => ((b, atts), [(map #2 ths, [])])));
isabelle