# HG changeset patch # User wenzelm # Date 1152613021 -7200 # Node ID def4ad161528d13e10799d038cdf7b16c90fc6ee # Parent a7e183bfebefeac84d5fdb4bd163f3cc6246d745 Name.invent_list; diff -r a7e183bfebef -r def4ad161528 src/Pure/Proof/proof_rewrite_rules.ML --- 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; diff -r a7e183bfebef -r def4ad161528 src/Pure/Syntax/syn_ext.ML --- 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) diff -r a7e183bfebef -r def4ad161528 src/Pure/Syntax/syn_trans.ML --- 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; diff -r a7e183bfebef -r def4ad161528 src/Pure/Tools/class_package.ML --- 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 "); diff -r a7e183bfebef -r def4ad161528 src/Pure/Tools/codegen_package.ML --- 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; diff -r a7e183bfebef -r def4ad161528 src/Pure/Tools/codegen_theorems.ML --- 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, diff -r a7e183bfebef -r def4ad161528 src/Pure/display.ML --- 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 diff -r a7e183bfebef -r def4ad161528 src/Pure/type_infer.ML --- 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)