intrn_arity: reject type abbreviations;

--- a/src/Pure/axclass.ML	Fri Apr 14 17:29:57 2000 +0200
+++ b/src/Pure/axclass.ML	Fri Apr 14 17:30:22 2000 +0200
@@ -360,8 +360,11 @@
 fun intrn_classrel sg c1_c2 =
   pairself (Sign.intern_class sg) c1_c2;
 
-fun intrn_arity intrn sg (t, Ss, x) =
-  (Sign.intern_tycon sg t, map (Sign.intern_sort sg) Ss, intrn sg x);
+fun intrn_arity intrn sg (raw_t, Ss, x) =
+  let val t = Sign.intern_tycon sg raw_t in
+    if Sign.is_type_abbr sg t then error ("Illegal type abbreviation: " ^ quote t)
+    else (t, map (Sign.intern_sort sg) Ss, intrn sg x)
+  end;
 
 
 fun ext_inst_subclass prep_classrel raw_c1_c2 names thms usr_tac thy =