1.1 --- a/src/Pure/Isar/class.ML	Thu Oct 04 19:54:47 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Thu Oct 04 20:29:13 2007 +0200
     1.3 @@ -87,7 +87,7 @@
     1.4  
     1.5  fun strip_all_ofclass thy sort =
     1.6    let
     1.7 -    val typ = TVar ((AxClass.param_tyvarname, 0), sort);
     1.8 +    val typ = TVar ((Name.aT, 0), sort);
     1.9      fun prem_inclass t =
    1.10        case Logic.strip_imp_prems t
    1.11         of ofcls :: _ => try Logic.dest_inclass ofcls
    1.12 @@ -264,7 +264,7 @@
    1.13      fun get_consts_sort (tyco, asorts, sort) =
    1.14        let
    1.15          val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort))
    1.16 -          (Name.names Name.context "'a" asorts))
    1.17 +          (Name.names Name.context Name.aT asorts))
    1.18        in maps (get_consts_class tyco ty) (Sign.complete_sort theory sort) end;
    1.19      val cs = maps get_consts_sort arities;
    1.20      fun mk_typnorm thy (ty, ty_sc) =
    1.21 @@ -474,7 +474,7 @@
    1.22       of SOME pred_intro => class_intro |> OF_LAST pred_intro
    1.23        | NONE => class_intro;
    1.24      val sort = Sign.super_classes thy class;
    1.25 -    val typ = TVar ((AxClass.param_tyvarname, 0), sort);
    1.26 +    val typ = TVar ((Name.aT, 0), sort);
    1.27      val defs = these_defs thy sups;
    1.28    in
    1.29      raw_intro
    1.30 @@ -504,7 +504,7 @@
    1.31          Locale.global_asms_of thy locale
    1.32          |> maps snd
    1.33          |> (map o map_aterms) (fn Free (s, _) => (the o Symtab.lookup insttab) s | t => t)
    1.34 -        |> (map o map_types o map_atyps) (fn TFree _ => TFree ("'a", [class1]) | T => T)
    1.35 +        |> (map o map_types o map_atyps) (fn TFree _ => TFree (Name.aT, [class1]) | T => T)
    1.36          |> map (ObjectLogic.ensure_propT thy)
    1.37        end;
    1.38      val (prems, concls) = pairself mk_axioms (class1, class2);
    1.39 @@ -578,7 +578,7 @@
    1.40          |> fst |> map fst
    1.41        handle TYPE (msg, _, _) => error msg;
    1.42      fun check_typ c idx ty = case (nth (Sign.const_typargs thy (c, ty)) idx) (*FIXME localize*)
    1.43 -     of TFree (v, _) => v = AxClass.param_tyvarname
    1.44 +     of TFree (v, _) => v = Name.aT
    1.45        | TVar (vi, _) => TypeInfer.is_param vi (*FIXME substitute in all typs*)
    1.46        | _ => false;
    1.47      fun subst_operation (t as Const (c, ty)) = (case local_operation c
    1.48 @@ -600,7 +600,7 @@
    1.49    in
    1.50      ctxt
    1.51      |> Variable.declare_term
    1.52 -        (Logic.mk_type (TFree (AxClass.param_tyvarname, local_sort)))
    1.53 +        (Logic.mk_type (TFree (Name.aT, local_sort)))
    1.54      |> get_remove_constraints sort
    1.55      |-> (fn constraints => Context.proof_map (Syntax.add_term_check 50 "class"
    1.56            (sort_term_check thy sort constraints)))
    1.57 @@ -640,7 +640,7 @@
    1.58        (map fst supparams);
    1.59      val mergeexpr = Locale.Merge (suplocales @ includes);
    1.60      val constrain = Element.Constrains ((map o apsnd o map_atyps)
    1.61 -      (fn TFree (_, sort) => TFree (AxClass.param_tyvarname, sort)) supparams);
    1.62 +      (fn TFree (_, sort) => TFree (Name.aT, sort)) supparams);
    1.63    in
    1.64      ProofContext.init thy
    1.65      |> Locale.cert_expr supexpr [constrain]
    1.66 @@ -662,7 +662,7 @@
    1.67        prep_spec thy raw_supclasses raw_includes_elems;
    1.68      val other_consts = map (prep_param thy) raw_other_consts;
    1.69      fun mk_instT class = Symtab.empty
    1.70 -      |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class]));
    1.71 +      |> Symtab.update (Name.aT, TFree (Name.aT, [class]));
    1.72      fun mk_inst class param_names cs =
    1.73        Symtab.empty
    1.74        |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
    1.75 @@ -680,7 +680,7 @@
    1.76              ^ Sign.string_of_sort thy supsort);
    1.77        in
    1.78          (local_sort, (map fst params, params
    1.79 -        |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, local_sort)))
    1.80 +        |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (Name.aT, local_sort)))
    1.81          |> (map o apsnd) (fork_mixfix true NONE #> fst)
    1.82          |> chop (length supconsts)
    1.83          |> snd))
    1.84 @@ -754,7 +754,7 @@
    1.85      val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) [class];
    1.86      val rhs' = export_fixes thy class rhs;
    1.87      val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
    1.88 -      if w = AxClass.param_tyvarname then TFree (w, constrain_sort sort) else TFree var);
    1.89 +      if w = Name.aT then TFree (w, constrain_sort sort) else TFree var);
    1.90      val ty' = Term.fastype_of rhs';
    1.91      val ty'' = subst_typ ty';
    1.92      val c' = mk_name c;
    1.93 @@ -765,7 +765,7 @@
    1.94          val def' = symmetric def;
    1.95          val def_eq = Thm.prop_of def';
    1.96          val typargs = Sign.const_typargs thy (c', fastype_of rhs);
    1.97 -        val typidx = find_index (fn TFree (w, _) => AxClass.param_tyvarname = w | _ => false) typargs;
    1.98 +        val typidx = find_index (fn TFree (w, _) => Name.aT = w | _ => false) typargs;
    1.99        in
   1.100          thy
   1.101          |> class_interpretation class [def'] [def_eq]
   1.102 @@ -787,7 +787,7 @@
   1.103    let
   1.104      val local_sort = (#local_sort o the_class_data thy) class;
   1.105      val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
   1.106 -      if w = AxClass.param_tyvarname then TFree (w, local_sort) else TFree var);
   1.107 +      if w = Name.aT then TFree (w, local_sort) else TFree var);
   1.108      val ty = fastype_of rhs;
   1.109      val rhs' = map_types subst_typ rhs;
   1.110    in
   1.111 @@ -821,7 +821,7 @@
   1.112              val ax = #axioms (AxClass.get_definition thy class1);
   1.113              val intro = #intro (AxClass.get_definition thy class2)
   1.114                |> Drule.instantiate' [SOME (Thm.ctyp_of thy
   1.115 -                  (TVar ((AxClass.param_tyvarname, 0), [class1])))] [];
   1.116 +                  (TVar ((Name.aT, 0), [class1])))] [];
   1.117              val thm =
   1.118                intro
   1.119                |> OF_LAST (interp OF ax)

     2.1 --- a/src/Pure/axclass.ML	Thu Oct 04 19:54:47 2007 +0200
     2.2 +++ b/src/Pure/axclass.ML	Thu Oct 04 20:29:13 2007 +0200
     2.3 @@ -23,7 +23,6 @@
     2.4    val class_intros: theory -> thm list
     2.5    val class_of_param: theory -> string -> class option
     2.6    val params_of_class: theory -> class -> string * (string * typ) list
     2.7 -  val param_tyvarname: string
     2.8    val print_axclasses: theory -> unit
     2.9    val cert_classrel: theory -> class * class -> class * class
    2.10    val read_classrel: theory -> xstring * xstring -> class * class
    2.11 @@ -65,8 +64,6 @@
    2.12  val superN = "super";
    2.13  val axiomsN = "axioms";
    2.14  
    2.15 -val param_tyvarname = "'a";
    2.16 -
    2.17  datatype axclass = AxClass of
    2.18   {def: thm,
    2.19    intro: thm,
    2.20 @@ -139,8 +136,7 @@
    2.21  fun class_of_param thy =
    2.22    AList.lookup (op =) (#2 (get_axclasses thy));
    2.23  
    2.24 -fun params_of_class thy class =
    2.25 -  (param_tyvarname, (#params o get_definition thy) class);
    2.26 +fun params_of_class thy class = (Name.aT, #params (get_definition thy class));
    2.27  
    2.28  
    2.29  (* maintain instances *)
    2.30 @@ -341,9 +337,10 @@
    2.31          val _ = case Term.typ_tvars ty
    2.32           of [_] => ()
    2.33            | _ => error ("Exactly one type variable required in parameter " ^ quote param);
    2.34 -        val ty' = Term.map_type_tvar (fn _ => TFree (param_tyvarname, [class])) ty;
    2.35 +        val ty' = Term.map_type_tvar (fn _ => TFree (Name.aT, [class])) ty;
    2.36        in (param, ty') end) params;
    2.37  
    2.38 +
    2.39      (* result *)
    2.40  
    2.41      val axclass = make_axclass ((def, intro, axioms), params_typs);