# HG changeset patch
# User wenzelm
# Date 1191522553 -7200
# Node ID bc15dcaed51707320730425a3b2a4b910b14df1d
# Parent  d8ff870a11ff37d10a4b0fecbbea5f9ca6a6b476
replaced AxClass.param_tyvarname by Name.aT;

diff -r d8ff870a11ff -r bc15dcaed517 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Oct 04 19:54:47 2007 +0200
+++ b/src/Pure/Isar/class.ML	Thu Oct 04 20:29:13 2007 +0200
@@ -87,7 +87,7 @@
 
 fun strip_all_ofclass thy sort =
   let
-    val typ = TVar ((AxClass.param_tyvarname, 0), sort);
+    val typ = TVar ((Name.aT, 0), sort);
     fun prem_inclass t =
       case Logic.strip_imp_prems t
        of ofcls :: _ => try Logic.dest_inclass ofcls
@@ -264,7 +264,7 @@
     fun get_consts_sort (tyco, asorts, sort) =
       let
         val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort))
-          (Name.names Name.context "'a" asorts))
+          (Name.names Name.context Name.aT asorts))
       in maps (get_consts_class tyco ty) (Sign.complete_sort theory sort) end;
     val cs = maps get_consts_sort arities;
     fun mk_typnorm thy (ty, ty_sc) =
@@ -474,7 +474,7 @@
      of SOME pred_intro => class_intro |> OF_LAST pred_intro
       | NONE => class_intro;
     val sort = Sign.super_classes thy class;
-    val typ = TVar ((AxClass.param_tyvarname, 0), sort);
+    val typ = TVar ((Name.aT, 0), sort);
     val defs = these_defs thy sups;
   in
     raw_intro
@@ -504,7 +504,7 @@
         Locale.global_asms_of thy locale
         |> maps snd
         |> (map o map_aterms) (fn Free (s, _) => (the o Symtab.lookup insttab) s | t => t)
-        |> (map o map_types o map_atyps) (fn TFree _ => TFree ("'a", [class1]) | T => T)
+        |> (map o map_types o map_atyps) (fn TFree _ => TFree (Name.aT, [class1]) | T => T)
         |> map (ObjectLogic.ensure_propT thy)
       end;
     val (prems, concls) = pairself mk_axioms (class1, class2);
@@ -578,7 +578,7 @@
         |> fst |> map fst
       handle TYPE (msg, _, _) => error msg;
     fun check_typ c idx ty = case (nth (Sign.const_typargs thy (c, ty)) idx) (*FIXME localize*)
-     of TFree (v, _) => v = AxClass.param_tyvarname
+     of TFree (v, _) => v = Name.aT
       | TVar (vi, _) => TypeInfer.is_param vi (*FIXME substitute in all typs*)
       | _ => false;
     fun subst_operation (t as Const (c, ty)) = (case local_operation c
@@ -600,7 +600,7 @@
   in
     ctxt
     |> Variable.declare_term
-        (Logic.mk_type (TFree (AxClass.param_tyvarname, local_sort)))
+        (Logic.mk_type (TFree (Name.aT, local_sort)))
     |> get_remove_constraints sort
     |-> (fn constraints => Context.proof_map (Syntax.add_term_check 50 "class"
           (sort_term_check thy sort constraints)))
@@ -640,7 +640,7 @@
       (map fst supparams);
     val mergeexpr = Locale.Merge (suplocales @ includes);
     val constrain = Element.Constrains ((map o apsnd o map_atyps)
-      (fn TFree (_, sort) => TFree (AxClass.param_tyvarname, sort)) supparams);
+      (fn TFree (_, sort) => TFree (Name.aT, sort)) supparams);
   in
     ProofContext.init thy
     |> Locale.cert_expr supexpr [constrain]
@@ -662,7 +662,7 @@
       prep_spec thy raw_supclasses raw_includes_elems;
     val other_consts = map (prep_param thy) raw_other_consts;
     fun mk_instT class = Symtab.empty
-      |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class]));
+      |> Symtab.update (Name.aT, TFree (Name.aT, [class]));
     fun mk_inst class param_names cs =
       Symtab.empty
       |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
@@ -680,7 +680,7 @@
             ^ Sign.string_of_sort thy supsort);
       in
         (local_sort, (map fst params, params
-        |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, local_sort)))
+        |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (Name.aT, local_sort)))
         |> (map o apsnd) (fork_mixfix true NONE #> fst)
         |> chop (length supconsts)
         |> snd))
@@ -754,7 +754,7 @@
     val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) [class];
     val rhs' = export_fixes thy class rhs;
     val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
-      if w = AxClass.param_tyvarname then TFree (w, constrain_sort sort) else TFree var);
+      if w = Name.aT then TFree (w, constrain_sort sort) else TFree var);
     val ty' = Term.fastype_of rhs';
     val ty'' = subst_typ ty';
     val c' = mk_name c;
@@ -765,7 +765,7 @@
         val def' = symmetric def;
         val def_eq = Thm.prop_of def';
         val typargs = Sign.const_typargs thy (c', fastype_of rhs);
-        val typidx = find_index (fn TFree (w, _) => AxClass.param_tyvarname = w | _ => false) typargs;
+        val typidx = find_index (fn TFree (w, _) => Name.aT = w | _ => false) typargs;
       in
         thy
         |> class_interpretation class [def'] [def_eq]
@@ -787,7 +787,7 @@
   let
     val local_sort = (#local_sort o the_class_data thy) class;
     val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
-      if w = AxClass.param_tyvarname then TFree (w, local_sort) else TFree var);
+      if w = Name.aT then TFree (w, local_sort) else TFree var);
     val ty = fastype_of rhs;
     val rhs' = map_types subst_typ rhs;
   in
@@ -821,7 +821,7 @@
             val ax = #axioms (AxClass.get_definition thy class1);
             val intro = #intro (AxClass.get_definition thy class2)
               |> Drule.instantiate' [SOME (Thm.ctyp_of thy
-                  (TVar ((AxClass.param_tyvarname, 0), [class1])))] [];
+                  (TVar ((Name.aT, 0), [class1])))] [];
             val thm =
               intro
               |> OF_LAST (interp OF ax)
diff -r d8ff870a11ff -r bc15dcaed517 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Thu Oct 04 19:54:47 2007 +0200
+++ b/src/Pure/axclass.ML	Thu Oct 04 20:29:13 2007 +0200
@@ -23,7 +23,6 @@
   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
@@ -65,8 +64,6 @@
 val superN = "super";
 val axiomsN = "axioms";
 
-val param_tyvarname = "'a";
-
 datatype axclass = AxClass of
  {def: thm,
   intro: thm,
@@ -139,8 +136,7 @@
 fun class_of_param thy =
   AList.lookup (op =) (#2 (get_axclasses thy));
 
-fun params_of_class thy class =
-  (param_tyvarname, (#params o get_definition thy) class);
+fun params_of_class thy class = (Name.aT, #params (get_definition thy class));
 
 
 (* maintain instances *)
@@ -341,9 +337,10 @@
         val _ = case Term.typ_tvars ty
          of [_] => ()
           | _ => error ("Exactly one type variable required in parameter " ^ quote param);
-        val ty' = Term.map_type_tvar (fn _ => TFree (param_tyvarname, [class])) ty;
+        val ty' = Term.map_type_tvar (fn _ => TFree (Name.aT, [class])) ty;
       in (param, ty') end) params;
 
+
     (* result *)
 
     val axclass = make_axclass ((def, intro, axioms), params_typs);