src/Pure/Isar/code.ML
changeset 24848 5dbbd33c3236
parent 24844 98c006a30218
child 24928 3419943838f5
     1.1 --- a/src/Pure/Isar/code.ML	Thu Oct 04 20:29:13 2007 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Thu Oct 04 20:29:24 2007 +0200
     1.3 @@ -579,9 +579,9 @@
     1.4  
     1.5  fun gen_classparam_typ constr thy class (c, tyco) = 
     1.6    let
     1.7 -    val (var, cs) = try (AxClass.params_of_class thy) class |> the_default ("'a", [])
     1.8 +    val (var, cs) = try (AxClass.params_of_class thy) class |> the_default (Name.aT, [])
     1.9      val ty = (the o AList.lookup (op =) cs) c;
    1.10 -    val sort_args = Name.names (Name.declare var Name.context) "'a"
    1.11 +    val sort_args = Name.names (Name.declare var Name.context) Name.aT
    1.12        (constr thy (class, tyco));
    1.13      val ty_inst = Type (tyco, map TFree sort_args);
    1.14    in Logic.varifyT (map_type_tfree (K ty_inst) ty) end;
    1.15 @@ -673,7 +673,7 @@
    1.16    case Symtab.lookup ((the_dtyps o the_exec) thy) tyco
    1.17     of SOME spec => spec
    1.18      | NONE => Sign.arity_number thy tyco
    1.19 -        |> Name.invents Name.context "'a"
    1.20 +        |> Name.invents Name.context Name.aT
    1.21          |> map (rpair [])
    1.22          |> rpair [];
    1.23  
    1.24 @@ -919,7 +919,7 @@
    1.25        (c, tyco) |> SOME
    1.26    | NONE => (case AxClass.class_of_param thy c
    1.27       of SOME class => SOME (Term.map_type_tvar
    1.28 -          (K (TVar (("'a", 0), [class]))) (Sign.the_const_type thy c))
    1.29 +          (K (TVar ((Name.aT, 0), [class]))) (Sign.the_const_type thy c))
    1.30        | NONE => get_constr_typ thy c);
    1.31  
    1.32  local