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 36106 19deea200358
parent 35894 ab6dc4d86ea1
child 36317 506d732cb522 
--- a/src/Pure/Isar/specification.ML	Sun Apr 11 14:06:35 2010 +0200
+++ b/src/Pure/Isar/specification.ML	Sun Apr 11 14:30:34 2010 +0200
@@ -173,7 +173,7 @@
         fold_map Thm.add_axiom
           (map (apfst (fn a => Binding.map_name (K a) b))
             (PureThy.name_multi (Name.of_binding b) (map subst props)))
-        #>> (fn ths => ((b, atts), [(ths, [])])));
+        #>> (fn ths => ((b, atts), [(map #2 ths, [])])));
 
     (*facts*)
     val (facts, facts_lthy) = axioms_thy
isabelle