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.
minor fix: instance now raises error if witness axioms don't exist;
authorwenzelm
Thu, 27 Jul 1995 13:13:32 +0200
changeset 1201 de2fc8cf9b6a
parent 1200 d4551b1a6da7
child 1202 968cd786a748
minor fix: instance now raises error if witness axioms don't exist;
src/Pure/axclass.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/axclass.ML	Wed Jul 26 17:35:23 1995 +0200
+++ b/src/Pure/axclass.ML	Thu Jul 27 13:13:32 1995 +0200
@@ -66,7 +66,7 @@
 val is_def = is_equals o #prop o rep_thm;
 
 fun witnesses thy axms thms =
-  get_axioms thy axms @ thms @ filter is_def (map snd (axioms_of thy));
+  map (get_axiom thy) axms @ thms @ filter is_def (map snd (axioms_of thy));
isabelle