# HG changeset patch
# User haftmann
# Date 1167420902 -3600
# Node ID ab834c5c38585bedb0b23bb7937a65678c9296d2
# Parent  dc9366853df18aafd69ec2771f95839be079b7ac
cleanup

diff -r dc9366853df1 -r ab834c5c3858 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Fri Dec 29 20:34:18 2006 +0100
+++ b/src/Pure/axclass.ML	Fri Dec 29 20:35:02 2006 +0100
@@ -13,6 +13,7 @@
   val class_intros: theory -> thm list
   val class_of_param: theory -> string -> class option
   val params_of_class: theory -> class -> string * (string * typ) list
+  val param_tyvarname: string
   val print_axclasses: theory -> unit
   val cert_classrel: theory -> class * class -> class * class
   val read_classrel: theory -> xstring * xstring -> class * class
@@ -340,7 +341,7 @@
         val ty = Sign.the_const_type thy param;
         val _ = case Term.typ_tvars ty
          of [_] => ()
-          | _ => error ("exactly one type variable required in parameter " ^ quote param);
+          | _ => error ("Exactly one type variable required in parameter " ^ quote param);
         val ty' = Term.map_type_tvar (fn _ => TFree (param_tyvarname, [class])) ty;
       in (param, ty') end) params;