src/Pure/axclass.ML
changeset 21953 ab834c5c3858
parent 21931 314f9e2a442c
child 22385 cc2be3315e72
     1.1 --- a/src/Pure/axclass.ML	Fri Dec 29 20:34:18 2006 +0100
     1.2 +++ b/src/Pure/axclass.ML	Fri Dec 29 20:35:02 2006 +0100
     1.3 @@ -13,6 +13,7 @@
     1.4    val class_intros: theory -> thm list
     1.5    val class_of_param: theory -> string -> class option
     1.6    val params_of_class: theory -> class -> string * (string * typ) list
     1.7 +  val param_tyvarname: string
     1.8    val print_axclasses: theory -> unit
     1.9    val cert_classrel: theory -> class * class -> class * class
    1.10    val read_classrel: theory -> xstring * xstring -> class * class
    1.11 @@ -340,7 +341,7 @@
    1.12          val ty = Sign.the_const_type thy param;
    1.13          val _ = case Term.typ_tvars ty
    1.14           of [_] => ()
    1.15 -          | _ => error ("exactly one type variable required in parameter " ^ quote param);
    1.16 +          | _ => error ("Exactly one type variable required in parameter " ^ quote param);
    1.17          val ty' = Term.map_type_tvar (fn _ => TFree (param_tyvarname, [class])) ty;
    1.18        in (param, ty') end) params;
    1.19