author | wenzelm |
Thu, 27 Jul 1995 13:13:32 +0200 | |
changeset 1201 | de2fc8cf9b6a |
parent 1200 | d4551b1a6da7 |
child 1202 | 968cd786a748 |
--- 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));