--- a/src/Pure/Proof/proof_rewrite_rules.ML Tue Jul 11 12:17:00 2006 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Tue Jul 11 12:17:01 2006 +0200
@@ -194,8 +194,7 @@
let
fun rew_term Ts t =
let
- val frees = map Free (variantlist
- (replicate (length Ts) "x", add_term_names (t, [])) ~~ Ts);
+ val frees = map Free (Name.invent_list (add_term_names (t, [])) "xa" (length Ts) ~~ Ts);
val t' = r (subst_bounds (frees, t));
fun strip [] t = t
| strip (_ :: xs) (Abs (_, _, t)) = strip xs t;
--- a/src/Pure/Syntax/syn_ext.ML Tue Jul 11 12:17:00 2006 +0200
+++ b/src/Pure/Syntax/syn_ext.ML Tue Jul 11 12:17:01 2006 +0200
@@ -297,7 +297,7 @@
val rangeT = Term.range_type typ handle Match =>
err_in_mfix "Missing structure argument for indexed syntax" mfix;
- val xs = map Ast.Variable (Term.invent_names [] "xa" (length args - 1));
+ val xs = map Ast.Variable (Name.invent_list [] "xa" (length args - 1));
val (xs1, xs2) = chop (find_index is_index args) xs;
val i = Ast.Variable "i";
val lhs = Ast.mk_appl (Ast.Constant indexed_const)
--- a/src/Pure/Syntax/syn_trans.ML Tue Jul 11 12:17:00 2006 +0200
+++ b/src/Pure/Syntax/syn_trans.ML Tue Jul 11 12:17:01 2006 +0200
@@ -384,7 +384,7 @@
(* dependent / nondependent quantifiers *)
fun variant_abs' (x, T, B) =
- let val x' = variant (add_term_names (B, [])) x in
+ let val x' = Name.variant (add_term_names (B, [])) x in
(x', subst_bound (mark_boundT (x', T), B))
end;
--- a/src/Pure/Tools/class_package.ML Tue Jul 11 12:17:00 2006 +0200
+++ b/src/Pure/Tools/class_package.ML Tue Jul 11 12:17:01 2006 +0200
@@ -174,7 +174,7 @@
val (clsvar, const_sign) = the_consts_sign thy class;
fun add_var sort used =
let
- val v = hd (Term.invent_names used "'a" 1)
+ val [v] = Name.invent_list used "'a" 1
in ((v, sort), v::used) end;
val (vsorts, _) =
[clsvar]
@@ -405,7 +405,8 @@
let
val pp = Sign.pp theory;
val arity as (tyco, asorts, sort) = prep_arity theory ((fn ((x, y), z) => (x, y, z)) raw_arity);
- val ty_inst = Type (tyco, map2 (curry TVar o rpair 0) (Term.invent_names [] "'a" (length asorts)) asorts)
+ val ty_inst =
+ Type (tyco, map2 (curry TVar o rpair 0) (Name.invent_list [] "'a" (length asorts)) asorts)
val name = case raw_name
of "" => Thm.def_name ((space_implode "_" o map NameSpace.base) sort ^ "_" ^ NameSpace.base tyco)
| _ => raw_name;
@@ -473,7 +474,7 @@
theory
|> fold_map get_remove_contraint (map fst cs)
||>> add_defs defs
- |-> (fn (cs, def_thms) =>
+ |-> (fn (cs, def_thms) =>
fold register_def def_thms
#> note_all
#> do_proof (after_qed cs) arity)
@@ -525,9 +526,10 @@
in (export_name, map (Name o NameSpace.append thm_name_base) prop_names) end;
val notes_tab_proto = map mk_thm_names prop_tab;
fun test_note thy thmref =
- can (Locale.note_thmss PureThy.corollaryK loc_name
+ can (Locale.note_thmss PureThy.corollaryK loc_name
[(("", []), [(thmref, [])])]) (Theory.copy thy);
- val notes_tab = map_filter (fn (export_name, thm_names) => case filter (test_note theory) thm_names
+ val notes_tab = map_filter (fn (export_name, thm_names) =>
+ case filter (test_note theory) thm_names
of [] => NONE
| thm_names' => SOME (export_name, thm_names')) notes_tab_proto;
val _ = writeln ("fishing for ");
--- a/src/Pure/Tools/codegen_package.ML Tue Jul 11 12:17:00 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML Tue Jul 11 12:17:01 2006 +0200
@@ -173,7 +173,7 @@
case (find_first (fn {lhs, ...} => Sign.typ_equiv thy (ty, lhs))
(Theory.definitions_of thy c))
of SOME {module, ...} => NameSpace.append module nsp_overl
- | NONE => if c = "op ="
+ | NONE => if c = "op =" (* FIXME depends on object-logic!? *)
then
NameSpace.append
((thyname_of_tyco thy o fst o dest_Type o hd o fst o strip_type) ty)
@@ -839,7 +839,7 @@
if length ts < imin then
let
val d = imin - length ts;
- val vs = Term.invent_names (add_term_names (Const (f, ty), [])) "x" d;
+ val vs = Name.invent_list (add_term_names (Const (f, ty), [])) "x" d;
val tys = Library.take (d, ((fst o strip_type) ty));
in
trns
@@ -936,8 +936,8 @@
val (ts', t) = split_last ts;
val (tys, dty) = (split_last o fst o strip_type) ty;
fun gen_names i =
- variantlist (replicate i "x", foldr add_term_names
- (map (fst o fst o dest_Var) (foldr add_term_vars [] ts)) ts);
+ Name.invent_list (foldr add_term_names
+ (map (fst o fst o dest_Var) (foldr add_term_vars [] ts)) ts) "xa" i;
fun cg_case_d (((cname, i), ty), t) trns =
let
val vs = gen_names i;
@@ -1012,7 +1012,7 @@
end) ((#2 o #constants o Consts.dest o #consts o Sign.rep_sg) thy)
|> (fn (overltab1, overltab2) =>
let
- val c = "op =";
+ val c = "op ="; (* FIXME depends on object-logic!? *)
val ty = Sign.the_const_type thy c;
fun inst tyco =
let
@@ -1020,7 +1020,7 @@
tyco
|> Symtab.lookup ((snd o #types o Type.rep_tsig o Sign.tsig_of) thy)
|> (fn SOME (Type.LogicalType i, _) => i)
- |> Term.invent_names [] "'a"
+ |> Name.invent_list [] "'a"
|> map (fn v => (TVar ((v, 0), Sign.defaultS thy)))
|> (fn tys => Type (tyco, tys))
in map_atyps (fn _ => ty_inst) ty end;
--- a/src/Pure/Tools/codegen_theorems.ML Tue Jul 11 12:17:00 2006 +0200
+++ b/src/Pure/Tools/codegen_theorems.ML Tue Jul 11 12:17:01 2006 +0200
@@ -216,7 +216,7 @@
val lhs = (fst o Logic.dest_equals) t;
val tys = (fst o strip_type o type_of) lhs;
val used = fold_aterms (fn Var ((v, _), _) => insert (op =) v | _ => I) lhs [];
- val vs = Term.invent_names used "x" (length tys);
+ val vs = Name.invent_list used "x" (length tys);
in
map2 (fn v => fn ty => Var ((v, 0), ty)) vs tys
end;
@@ -676,7 +676,7 @@
fun mk_lhs vs ((co1, tys1), (co2, tys2)) =
let
val dty = Type (dtco, map TFree vs);
- val (xs1, xs2) = chop (length tys1) (Term.invent_names [] "x" (length tys1 + length tys2));
+ val (xs1, xs2) = chop (length tys1) (Name.invent_list [] "x" (length tys1 + length tys2));
val frees1 = map2 (fn x => fn ty => Free (x, ty)) xs1 tys1;
val frees2 = map2 (fn x => fn ty => Free (x, ty)) xs2 tys2;
fun zip_co co xs tys = list_comb (Const (co,
--- a/src/Pure/display.ML Tue Jul 11 12:17:00 2006 +0200
+++ b/src/Pure/display.ML Tue Jul 11 12:17:01 2006 +0200
@@ -191,7 +191,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 (Term.invent_names [] "'a" n))))
+ else SOME (prt_typ (Type (t, tfrees (Name.invent_list [] "'a" n))))
| pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) =
if syn <> syn' then NONE
else SOME (Pretty.block
--- a/src/Pure/type_infer.ML Tue Jul 11 12:17:00 2006 +0200
+++ b/src/Pure/type_infer.ML Tue Jul 11 12:17:01 2006 +0200
@@ -245,7 +245,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 = Term.invent_names used' (prfx ^ "'a") (length parms);
+ val names = Name.invent_list used' (prfx ^ "'a") (length parms);
in
ListPair.app elim (parms, names);
(map simple_typ_of Ts, map simple_term_of ts)