# HG changeset patch
# User wenzelm
# Date 955726222 -7200
# Node ID 49ac76cf0d54379b3aed4740a0cecc101a522387
# Parent  2cdabe1bb35010e62f18d9b8f6dc52e8242dda9e
intrn_arity: reject type abbreviations;

diff -r 2cdabe1bb350 -r 49ac76cf0d54 src/Pure/axclass.ML
--- 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 =