replaced literal 'a by Name.aT;
authorwenzelm
Thu Oct 04 20:29:24 2007 +0200 (2007-10-04)
changeset 248485dbbd33c3236
parent 24847 bc15dcaed517
child 24849 193a10e6bf90
replaced literal 'a by Name.aT;
src/Pure/Isar/code.ML
src/Pure/Isar/code_unit.ML
src/Pure/Isar/instance.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/theory_target.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/display.ML
src/Pure/drule.ML
src/Pure/logic.ML
src/Pure/thm.ML
src/Pure/type.ML
src/Pure/type_infer.ML
src/Pure/variable.ML
     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
     2.1 --- a/src/Pure/Isar/code_unit.ML	Thu Oct 04 20:29:13 2007 +0200
     2.2 +++ b/src/Pure/Isar/code_unit.ML	Thu Oct 04 20:29:24 2007 +0200
     2.3 @@ -140,7 +140,7 @@
     2.4        in (c, (fst o strip_type) ty') end;
     2.5      val c' :: cs' = map ty_sorts cs;
     2.6      val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
     2.7 -    val vs = Name.names Name.context "'a" sorts;
     2.8 +    val vs = Name.names Name.context Name.aT sorts;
     2.9      val cs''' = map (inst vs) cs'';
    2.10    in (tyco, (vs, cs''')) end;
    2.11  
     3.1 --- a/src/Pure/Isar/instance.ML	Thu Oct 04 20:29:13 2007 +0200
     3.2 +++ b/src/Pure/Isar/instance.ML	Thu Oct 04 20:29:24 2007 +0200
     3.3 @@ -30,7 +30,8 @@
     3.4      fun prep_arity' raw_arity names =
     3.5        let
     3.6          val arity as (tyco, sorts, sort) = prep_arity thy raw_arity;
     3.7 -        val (vs, names') = Name.variants (replicate (length sorts) "'a") names;
     3.8 +        val vs = Name.invents names Name.aT (length sorts);
     3.9 +        val names' = fold Name.declare vs names;
    3.10        in (((tyco, vs ~~ sorts), sort), names') end;
    3.11      val (arities, _) = fold_map prep_arity' raw_arities Name.context;
    3.12      fun get_param tyco ty_subst (param, (c, ty)) =
     4.1 --- a/src/Pure/Isar/object_logic.ML	Thu Oct 04 20:29:13 2007 +0200
     4.2 +++ b/src/Pure/Isar/object_logic.ML	Thu Oct 04 20:29:24 2007 +0200
     4.3 @@ -99,7 +99,7 @@
     4.4  fun fixed_judgment thy x =
     4.5    let  (*be robust wrt. low-level errors*)
     4.6      val c = judgment_name thy;
     4.7 -    val aT = TFree ("'a", []);
     4.8 +    val aT = TFree (Name.aT, []);
     4.9      val T =
    4.10        the_default (aT --> propT) (Sign.const_type thy c)
    4.11        |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
     5.1 --- a/src/Pure/Isar/specification.ML	Thu Oct 04 20:29:13 2007 +0200
     5.2 +++ b/src/Pure/Isar/specification.ML	Thu Oct 04 20:29:24 2007 +0200
     5.3 @@ -89,7 +89,7 @@
     5.4        (case duplicates (op =) commons of [] => ()
     5.5        | dups => error ("Duplicate local variables " ^ commas_quote dups));
     5.6      val frees = rev ((fold o fold_aterms) add_free As (rev commons));
     5.7 -    val types = map (TypeInfer.param i o rpair []) (Name.invents Name.context "'a" (length frees));
     5.8 +    val types = map (TypeInfer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
     5.9      val uniform_typing = the o AList.lookup (op =) (frees ~~ types);
    5.10  
    5.11      fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
     6.1 --- a/src/Pure/Isar/theory_target.ML	Thu Oct 04 20:29:13 2007 +0200
     6.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Oct 04 20:29:24 2007 +0200
     6.3 @@ -211,7 +211,7 @@
     6.4  fun add_def_new (name, prop) thy =  (* FIXME inactive --- breaks codegen *)
     6.5    let
     6.6      val tfrees = rev (map TFree (Term.add_tfrees prop []));
     6.7 -    val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context "'a" (length tfrees));
     6.8 +    val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
     6.9      val strip_sorts = tfrees ~~ tfrees';
    6.10      val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT)) (tfrees' ~~ tfrees);
    6.11  
     7.1 --- a/src/Pure/Proof/proof_syntax.ML	Thu Oct 04 20:29:13 2007 +0200
     7.2 +++ b/src/Pure/Proof/proof_syntax.ML	Thu Oct 04 20:29:24 2007 +0200
     7.3 @@ -35,7 +35,7 @@
     7.4  val paramT = Type ("param", []);
     7.5  val paramsT = Type ("params", []);
     7.6  val idtT = Type ("idt", []);
     7.7 -val aT = TFree ("'a", []);
     7.8 +val aT = TFree (Name.aT, []);
     7.9  
    7.10  (** constants for theorems and axioms **)
    7.11  
     8.1 --- a/src/Pure/display.ML	Thu Oct 04 20:29:13 2007 +0200
     8.2 +++ b/src/Pure/display.ML	Thu Oct 04 20:29:24 2007 +0200
     8.3 @@ -172,7 +172,7 @@
     8.4      val tfrees = map (fn v => TFree (v, []));
     8.5      fun pretty_type syn (t, (Type.LogicalType n, _)) =
     8.6            if syn then NONE
     8.7 -          else SOME (prt_typ (Type (t, tfrees (Name.invent_list [] "'a" n))))
     8.8 +          else SOME (prt_typ (Type (t, tfrees (Name.invents Name.context Name.aT n))))
     8.9        | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) =
    8.10            if syn <> syn' then NONE
    8.11            else SOME (Pretty.block
     9.1 --- a/src/Pure/drule.ML	Thu Oct 04 20:29:13 2007 +0200
     9.2 +++ b/src/Pure/drule.ML	Thu Oct 04 20:29:24 2007 +0200
     9.3 @@ -272,7 +272,7 @@
     9.4      val cT = certT T;
     9.5      fun class_triv c =
     9.6        Thm.class_triv thy c
     9.7 -      |> Thm.instantiate ([(certT (TVar (("'a", 0), [c])), cT)], []);
     9.8 +      |> Thm.instantiate ([(certT (TVar ((Name.aT, 0), [c])), cT)], []);
     9.9    in map class_triv S end;
    9.10  
    9.11  fun unconstrainTs th =
    10.1 --- a/src/Pure/logic.ML	Thu Oct 04 20:29:13 2007 +0200
    10.2 +++ b/src/Pure/logic.ML	Thu Oct 04 20:29:24 2007 +0200
    10.3 @@ -238,7 +238,7 @@
    10.4  fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
    10.5  
    10.6  fun mk_arities (t, Ss, S) =
    10.7 -  let val T = Type (t, ListPair.map TFree (Name.invent_list [] "'a" (length Ss), Ss))
    10.8 +  let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (length Ss), Ss))
    10.9    in map (fn c => mk_inclass (T, c)) S end;
   10.10  
   10.11  fun dest_arity tm =
    11.1 --- a/src/Pure/thm.ML	Thu Oct 04 20:29:13 2007 +0200
    11.2 +++ b/src/Pure/thm.ML	Thu Oct 04 20:29:24 2007 +0200
    11.3 @@ -1144,7 +1144,7 @@
    11.4  fun class_triv thy c =
    11.5    let
    11.6      val Cterm {t, maxidx, sorts, ...} =
    11.7 -      cterm_of thy (Logic.mk_inclass (TVar (("'a", 0), [c]), Sign.certify_class thy c))
    11.8 +      cterm_of thy (Logic.mk_inclass (TVar ((Name.aT, 0), [c]), Sign.certify_class thy c))
    11.9          handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
   11.10      val der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME []));
   11.11    in
    12.1 --- a/src/Pure/type.ML	Thu Oct 04 20:29:13 2007 +0200
    12.2 +++ b/src/Pure/type.ML	Thu Oct 04 20:29:24 2007 +0200
    12.3 @@ -396,7 +396,7 @@
    12.4  fun unify (tsig as TSig {classes = (_, classes), ...}) TU (tyenv, maxidx) =
    12.5    let
    12.6      val tyvar_count = ref maxidx;
    12.7 -    fun gen_tyvar S = TVar (("'a", inc tyvar_count), S);
    12.8 +    fun gen_tyvar S = TVar ((Name.aT, inc tyvar_count), S);
    12.9  
   12.10      fun mg_domain a S = Sorts.mg_domain classes a S
   12.11        handle Sorts.CLASS_ERROR _ => raise TUNIFY;
    13.1 --- a/src/Pure/type_infer.ML	Thu Oct 04 20:29:13 2007 +0200
    13.2 +++ b/src/Pure/type_infer.ML	Thu Oct 04 20:29:24 2007 +0200
    13.3 @@ -61,7 +61,7 @@
    13.4      fun subst_param (xi, S) (inst, used) =
    13.5        if is_param xi then
    13.6          let
    13.7 -          val [a] = Name.invents used "'a" 1;
    13.8 +          val [a] = Name.invents used Name.aT 1;
    13.9            val used' = Name.declare a used;
   13.10          in (((xi, S), TFree (a, S)) :: inst, used') end
   13.11        else (inst, used);
   13.12 @@ -237,7 +237,7 @@
   13.13  
   13.14      val used' = fold add_names ts (fold add_namesT Ts used);
   13.15      val parms = rev (fold add_parms ts (fold add_parmsT Ts []));
   13.16 -    val names = Name.invents used' (prfx ^ "'a") (length parms);
   13.17 +    val names = Name.invents used' (prfx ^ Name.aT) (length parms);
   13.18    in
   13.19      ListPair.app elim (parms, names);
   13.20      (map simple_typ_of Ts, map simple_term_of ts)
    14.1 --- a/src/Pure/variable.ML	Thu Oct 04 20:29:13 2007 +0200
    14.2 +++ b/src/Pure/variable.ML	Thu Oct 04 20:29:24 2007 +0200
    14.3 @@ -299,7 +299,7 @@
    14.4  
    14.5  fun invent_types Ss ctxt =
    14.6    let
    14.7 -    val tfrees = Name.invents (names_of ctxt) "'a" (length Ss) ~~ Ss;
    14.8 +    val tfrees = Name.invents (names_of ctxt) Name.aT (length Ss) ~~ Ss;
    14.9      val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
   14.10    in (tfrees, ctxt') end;
   14.11