# HG changeset patch
# User wenzelm
# Date 1191522564 -7200
# Node ID 5dbbd33c32366e3a26d9a3d81f80eeb953a0cb0f
# Parent  bc15dcaed51707320730425a3b2a4b910b14df1d
replaced literal 'a by Name.aT;

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
diff -r bc15dcaed517 -r 5dbbd33c3236 src/Pure/Isar/code_unit.ML
--- a/src/Pure/Isar/code_unit.ML	Thu Oct 04 20:29:13 2007 +0200
+++ b/src/Pure/Isar/code_unit.ML	Thu Oct 04 20:29:24 2007 +0200
@@ -140,7 +140,7 @@
       in (c, (fst o strip_type) ty') end;
     val c' :: cs' = map ty_sorts cs;
     val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
-    val vs = Name.names Name.context "'a" sorts;
+    val vs = Name.names Name.context Name.aT sorts;
     val cs''' = map (inst vs) cs'';
   in (tyco, (vs, cs''')) end;
 
diff -r bc15dcaed517 -r 5dbbd33c3236 src/Pure/Isar/instance.ML
--- a/src/Pure/Isar/instance.ML	Thu Oct 04 20:29:13 2007 +0200
+++ b/src/Pure/Isar/instance.ML	Thu Oct 04 20:29:24 2007 +0200
@@ -30,7 +30,8 @@
     fun prep_arity' raw_arity names =
       let
         val arity as (tyco, sorts, sort) = prep_arity thy raw_arity;
-        val (vs, names') = Name.variants (replicate (length sorts) "'a") names;
+        val vs = Name.invents names Name.aT (length sorts);
+        val names' = fold Name.declare vs names;
       in (((tyco, vs ~~ sorts), sort), names') end;
     val (arities, _) = fold_map prep_arity' raw_arities Name.context;
     fun get_param tyco ty_subst (param, (c, ty)) =
diff -r bc15dcaed517 -r 5dbbd33c3236 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Thu Oct 04 20:29:13 2007 +0200
+++ b/src/Pure/Isar/object_logic.ML	Thu Oct 04 20:29:24 2007 +0200
@@ -99,7 +99,7 @@
 fun fixed_judgment thy x =
   let  (*be robust wrt. low-level errors*)
     val c = judgment_name thy;
-    val aT = TFree ("'a", []);
+    val aT = TFree (Name.aT, []);
     val T =
       the_default (aT --> propT) (Sign.const_type thy c)
       |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
diff -r bc15dcaed517 -r 5dbbd33c3236 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Thu Oct 04 20:29:13 2007 +0200
+++ b/src/Pure/Isar/specification.ML	Thu Oct 04 20:29:24 2007 +0200
@@ -89,7 +89,7 @@
       (case duplicates (op =) commons of [] => ()
       | dups => error ("Duplicate local variables " ^ commas_quote dups));
     val frees = rev ((fold o fold_aterms) add_free As (rev commons));
-    val types = map (TypeInfer.param i o rpair []) (Name.invents Name.context "'a" (length frees));
+    val types = map (TypeInfer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
     val uniform_typing = the o AList.lookup (op =) (frees ~~ types);
 
     fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
diff -r bc15dcaed517 -r 5dbbd33c3236 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Thu Oct 04 20:29:13 2007 +0200
+++ b/src/Pure/Isar/theory_target.ML	Thu Oct 04 20:29:24 2007 +0200
@@ -211,7 +211,7 @@
 fun add_def_new (name, prop) thy =  (* FIXME inactive --- breaks codegen *)
   let
     val tfrees = rev (map TFree (Term.add_tfrees prop []));
-    val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context "'a" (length tfrees));
+    val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
     val strip_sorts = tfrees ~~ tfrees';
     val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT)) (tfrees' ~~ tfrees);
 
diff -r bc15dcaed517 -r 5dbbd33c3236 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Thu Oct 04 20:29:13 2007 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Thu Oct 04 20:29:24 2007 +0200
@@ -35,7 +35,7 @@
 val paramT = Type ("param", []);
 val paramsT = Type ("params", []);
 val idtT = Type ("idt", []);
-val aT = TFree ("'a", []);
+val aT = TFree (Name.aT, []);
 
 (** constants for theorems and axioms **)
 
diff -r bc15dcaed517 -r 5dbbd33c3236 src/Pure/display.ML
--- a/src/Pure/display.ML	Thu Oct 04 20:29:13 2007 +0200
+++ b/src/Pure/display.ML	Thu Oct 04 20:29:24 2007 +0200
@@ -172,7 +172,7 @@
     val tfrees = map (fn v => TFree (v, []));
     fun pretty_type syn (t, (Type.LogicalType n, _)) =
           if syn then NONE
-          else SOME (prt_typ (Type (t, tfrees (Name.invent_list [] "'a" n))))
+          else SOME (prt_typ (Type (t, tfrees (Name.invents Name.context Name.aT n))))
       | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) =
           if syn <> syn' then NONE
           else SOME (Pretty.block
diff -r bc15dcaed517 -r 5dbbd33c3236 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Oct 04 20:29:13 2007 +0200
+++ b/src/Pure/drule.ML	Thu Oct 04 20:29:24 2007 +0200
@@ -272,7 +272,7 @@
     val cT = certT T;
     fun class_triv c =
       Thm.class_triv thy c
-      |> Thm.instantiate ([(certT (TVar (("'a", 0), [c])), cT)], []);
+      |> Thm.instantiate ([(certT (TVar ((Name.aT, 0), [c])), cT)], []);
   in map class_triv S end;
 
 fun unconstrainTs th =
diff -r bc15dcaed517 -r 5dbbd33c3236 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Thu Oct 04 20:29:13 2007 +0200
+++ b/src/Pure/logic.ML	Thu Oct 04 20:29:24 2007 +0200
@@ -238,7 +238,7 @@
 fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
 
 fun mk_arities (t, Ss, S) =
-  let val T = Type (t, ListPair.map TFree (Name.invent_list [] "'a" (length Ss), Ss))
+  let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (length Ss), Ss))
   in map (fn c => mk_inclass (T, c)) S end;
 
 fun dest_arity tm =
diff -r bc15dcaed517 -r 5dbbd33c3236 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Oct 04 20:29:13 2007 +0200
+++ b/src/Pure/thm.ML	Thu Oct 04 20:29:24 2007 +0200
@@ -1144,7 +1144,7 @@
 fun class_triv thy c =
   let
     val Cterm {t, maxidx, sorts, ...} =
-      cterm_of thy (Logic.mk_inclass (TVar (("'a", 0), [c]), Sign.certify_class thy c))
+      cterm_of thy (Logic.mk_inclass (TVar ((Name.aT, 0), [c]), Sign.certify_class thy c))
         handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
     val der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME []));
   in
diff -r bc15dcaed517 -r 5dbbd33c3236 src/Pure/type.ML
--- a/src/Pure/type.ML	Thu Oct 04 20:29:13 2007 +0200
+++ b/src/Pure/type.ML	Thu Oct 04 20:29:24 2007 +0200
@@ -396,7 +396,7 @@
 fun unify (tsig as TSig {classes = (_, classes), ...}) TU (tyenv, maxidx) =
   let
     val tyvar_count = ref maxidx;
-    fun gen_tyvar S = TVar (("'a", inc tyvar_count), S);
+    fun gen_tyvar S = TVar ((Name.aT, inc tyvar_count), S);
 
     fun mg_domain a S = Sorts.mg_domain classes a S
       handle Sorts.CLASS_ERROR _ => raise TUNIFY;
diff -r bc15dcaed517 -r 5dbbd33c3236 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Thu Oct 04 20:29:13 2007 +0200
+++ b/src/Pure/type_infer.ML	Thu Oct 04 20:29:24 2007 +0200
@@ -61,7 +61,7 @@
     fun subst_param (xi, S) (inst, used) =
       if is_param xi then
         let
-          val [a] = Name.invents used "'a" 1;
+          val [a] = Name.invents used Name.aT 1;
           val used' = Name.declare a used;
         in (((xi, S), TFree (a, S)) :: inst, used') end
       else (inst, used);
@@ -237,7 +237,7 @@
 
     val used' = fold add_names ts (fold add_namesT Ts used);
     val parms = rev (fold add_parms ts (fold add_parmsT Ts []));
-    val names = Name.invents used' (prfx ^ "'a") (length parms);
+    val names = Name.invents used' (prfx ^ Name.aT) (length parms);
   in
     ListPair.app elim (parms, names);
     (map simple_typ_of Ts, map simple_term_of ts)
diff -r bc15dcaed517 -r 5dbbd33c3236 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Thu Oct 04 20:29:13 2007 +0200
+++ b/src/Pure/variable.ML	Thu Oct 04 20:29:24 2007 +0200
@@ -299,7 +299,7 @@
 
 fun invent_types Ss ctxt =
   let
-    val tfrees = Name.invents (names_of ctxt) "'a" (length Ss) ~~ Ss;
+    val tfrees = Name.invents (names_of ctxt) Name.aT (length Ss) ~~ Ss;
     val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
   in (tfrees, ctxt') end;