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