src/Pure/axclass.ML
changeset 1201 de2fc8cf9b6a
parent 886 9af08725600b
child 1217 f96a04c6b352
--- 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));