src/Pure/axclass.ML
changeset 8716 49ac76cf0d54
parent 8671 6ce91a80f616
child 8720 840c75ab2a7f
     1.1 --- a/src/Pure/axclass.ML	Fri Apr 14 17:29:57 2000 +0200
     1.2 +++ b/src/Pure/axclass.ML	Fri Apr 14 17:30:22 2000 +0200
     1.3 @@ -360,8 +360,11 @@
     1.4  fun intrn_classrel sg c1_c2 =
     1.5    pairself (Sign.intern_class sg) c1_c2;
     1.6  
     1.7 -fun intrn_arity intrn sg (t, Ss, x) =
     1.8 -  (Sign.intern_tycon sg t, map (Sign.intern_sort sg) Ss, intrn sg x);
     1.9 +fun intrn_arity intrn sg (raw_t, Ss, x) =
    1.10 +  let val t = Sign.intern_tycon sg raw_t in
    1.11 +    if Sign.is_type_abbr sg t then error ("Illegal type abbreviation: " ^ quote t)
    1.12 +    else (t, map (Sign.intern_sort sg) Ss, intrn sg x)
    1.13 +  end;
    1.14  
    1.15  
    1.16  fun ext_inst_subclass prep_classrel raw_c1_c2 names thms usr_tac thy =