diff -r bc15dcaed517 -r 5dbbd33c3236 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Oct 04 20:29:13 2007 +0200
+++ b/src/Pure/Isar/code.ML	Thu Oct 04 20:29:24 2007 +0200
@@ -579,9 +579,9 @@
 
 fun gen_classparam_typ constr thy class (c, tyco) = 
   let
-    val (var, cs) = try (AxClass.params_of_class thy) class |> the_default ("'a", [])
+    val (var, cs) = try (AxClass.params_of_class thy) class |> the_default (Name.aT, [])
     val ty = (the o AList.lookup (op =) cs) c;
-    val sort_args = Name.names (Name.declare var Name.context) "'a"
+    val sort_args = Name.names (Name.declare var Name.context) Name.aT
       (constr thy (class, tyco));
     val ty_inst = Type (tyco, map TFree sort_args);
   in Logic.varifyT (map_type_tfree (K ty_inst) ty) end;
@@ -673,7 +673,7 @@
   case Symtab.lookup ((the_dtyps o the_exec) thy) tyco
    of SOME spec => spec
     | NONE => Sign.arity_number thy tyco
-        |> Name.invents Name.context "'a"
+        |> Name.invents Name.context Name.aT
         |> map (rpair [])
         |> rpair [];
 
@@ -919,7 +919,7 @@
       (c, tyco) |> SOME
   | NONE => (case AxClass.class_of_param thy c
      of SOME class => SOME (Term.map_type_tvar
-          (K (TVar (("'a", 0), [class]))) (Sign.the_const_type thy c))
+          (K (TVar ((Name.aT, 0), [class]))) (Sign.the_const_type thy c))
       | NONE => get_constr_typ thy c);
 
 local