| 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));