src/Pure/axclass.ML
changeset 25605 35a5f7f4b97b
parent 25597 34860182b250
child 25617 b495384e48e1
     1.1 --- a/src/Pure/axclass.ML	Tue Dec 11 10:23:11 2007 +0100
     1.2 +++ b/src/Pure/axclass.ML	Tue Dec 11 10:23:12 2007 +0100
     1.3 @@ -327,8 +327,13 @@
     1.4  
     1.5  fun declare_overloaded (c, T) thy =
     1.6    let
     1.7 -    val SOME class = class_of_param thy c;
     1.8 -    val SOME tyco = inst_tyco_of thy (c, T);
     1.9 +    val class = case class_of_param thy c
    1.10 +     of SOME class => class
    1.11 +      | NONE => error ("Not a class parameter: " ^ quote c);
    1.12 +    val tyco = case inst_tyco_of thy (c, T)
    1.13 +     of SOME tyco => tyco
    1.14 +      | NONE => error ("Illegal type for instantiation of class parameter: "
    1.15 +        ^ quote (c ^ " :: " ^ Sign.string_of_typ thy T));
    1.16      val name_inst = instance_name (tyco, class) ^ "_inst";
    1.17      val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
    1.18      val T' = Type.strip_sorts T;