changeset 17756 | d4a35f82fbb4 |
parent 17703 | 6ec36bad47ea |
child 17855 | 64c832a03a15 |
--- a/src/Pure/axclass.ML Tue Oct 04 16:47:40 2005 +0200 +++ b/src/Pure/axclass.ML Tue Oct 04 19:01:37 2005 +0200 @@ -192,7 +192,7 @@ if null (term_tfrees ax) then Logic.mk_implies (Logic.mk_inclass (aT [], class), ax) else map_term_tfrees (K (aT [class])) ax; - val abs_axms = map (abs_axm o #2) axms; + val abs_axms = map (abs_axm o snd) axms; fun axm_sort (name, ax) = (case term_tfrees ax of