src/Pure/axclass.ML

       | [(_, S)] =>
           if Sign.subsort sign ([class], S) then S
           else err_bad_axsort name class
       | _ => err_bad_tfrees name);
 
-    val axS = Sign.norm_sort sign (logicC :: flat (map axm_sort axioms));
+    val axS = Sign.norm_sort sign (logicC :: List.concat(map axm_sort axioms))
 
     val int_axm = Logic.close_form o map_term_tfrees (K (aT axS));
     fun inclass c = Logic.mk_inclass (aT axS, c);
 
     val intro_axm = Logic.list_implies