--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Thu Jun 09 16:34:49 2011 +0200
@@ -403,7 +403,7 @@
(* calculate function arguments of case combinator *)
val tns = map fst (Term.add_tfreesT lhsT [])
- val resultT = TFree (Name.variant tns "'t", @{sort pcpo})
+ val resultT = TFree (singleton (Name.variant_list tns) "'t", @{sort pcpo})
fun fTs T = map (fn (_, args) => map snd args -->> T) spec
val fns = Datatype_Prop.indexify_names (map (K "f") spec)
val fs = map Free (fns ~~ fTs resultT)
@@ -768,7 +768,7 @@
val resultT : typ =
let
val ts : string list = map fst (Term.add_tfreesT lhsT [])
- val t : string = Name.variant ts "'t"
+ val t : string = singleton (Name.variant_list ts) "'t"
in TFree (t, @{sort pcpo}) end
(* define match combinators *)
--- a/src/HOL/HOLCF/Tools/fixrec.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Thu Jun 09 16:34:49 2011 +0200
@@ -234,7 +234,7 @@
in comp_con T f rhs' (v::vs) taken' end
| Const (c, cT) =>
let
- val n = Name.variant taken "v"
+ val n = singleton (Name.variant_list taken) "v"
val v = Free(n, T)
val m = Const(match_name c, matcherT (cT, fastype_of rhs))
val k = big_lambdas vs rhs
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Thu Jun 09 16:34:49 2011 +0200
@@ -531,7 +531,7 @@
(* prove strictness and reduction rules of pattern combinators *)
local
val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
- val rn = Name.variant tns "'r";
+ val rn = singleton (Name.variant_list tns) "'r";
val R = TFree (rn, @{sort pcpo});
fun pat_lhs (pat, args) =
let
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Jun 09 16:34:49 2011 +0200
@@ -618,7 +618,6 @@
open Code_Thingol;
fun imp_program naming =
-
let
fun is_const c = case lookup_const naming c
of SOME c' => (fn c'' => c' = c'')
@@ -635,7 +634,7 @@
| dest_abs (t, ty) =
let
val vs = fold_varnames cons t [];
- val v = Name.variant vs "x";
+ val v = singleton (Name.variant_list vs) "x";
val ty' = (hd o fst o unfold_fun) ty;
in ((SOME v, ty'), t `$ IVar (SOME v)) end;
fun force (t as IConst (c, _) `$ t') = if is_return c
--- a/src/HOL/Import/hol4rews.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Import/hol4rews.ML Thu Jun 09 16:34:49 2011 +0200
@@ -605,7 +605,7 @@
then F defname (* name_def *)
else if not (member (op =) used pdefname)
then F pdefname (* name_primdef *)
- else F (Name.variant used pdefname) (* last resort *)
+ else F (singleton (Name.variant_list used) pdefname) (* last resort *)
end
end
--- a/src/HOL/Import/shuffler.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Import/shuffler.ML Thu Jun 09 16:34:49 2011 +0200
@@ -228,7 +228,7 @@
val (type_inst,_) =
fold (fn (w as (v,_), S) => fn (inst, used) =>
let
- val v' = Name.variant used v
+ val v' = singleton (Name.variant_list used) v
in
((w,TFree(v',S))::inst,v'::used)
end)
@@ -298,7 +298,7 @@
then
let
val cert = cterm_of thy
- val v = Free (Name.variant (Term.add_free_names t []) "v", xT)
+ val v = Free (singleton (Name.variant_list (Term.add_free_names t [])) "v", xT)
val cv = cert v
val ct = cert t
val th = (Thm.assume ct)
@@ -361,7 +361,7 @@
Type("fun",[aT,bT]) =>
let
val cert = cterm_of thy
- val vname = Name.variant (Term.add_free_names t []) "v"
+ val vname = singleton (Name.variant_list (Term.add_free_names t [])) "v"
val v = Free(vname,aT)
val cv = cert v
val ct = cert t
--- a/src/HOL/Inductive.thy Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Inductive.thy Thu Jun 09 16:34:49 2011 +0200
@@ -295,7 +295,8 @@
let
fun fun_tr ctxt [cs] =
let
- val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
+ (* FIXME proper name context!? *)
+ val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT);
val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr ctxt [x, cs];
in lambda x ft end
in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
--- a/src/HOL/Library/Efficient_Nat.thy Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Thu Jun 09 16:34:49 2011 +0200
@@ -113,8 +113,8 @@
fun remove_suc thy thms =
let
- val vname = Name.variant (map fst
- (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "n";
+ val vname = singleton (Name.variant_list (map fst
+ (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
fun lhs_of th = snd (Thm.dest_comb
(fst (Thm.dest_comb (cprop_of th))));
@@ -166,8 +166,8 @@
fun remove_suc_clause thy thms =
let
- val vname = Name.variant (map fst
- (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
+ val vname = singleton (Name.variant_list (map fst
+ (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "x";
fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v)
| find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
| find_var _ = NONE;
--- a/src/HOL/List.thy Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/List.thy Thu Jun 09 16:34:49 2011 +0200
@@ -383,7 +383,8 @@
fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
let
- val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
+ (* FIXME proper name context!? *)
+ val x = Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);
val e = if opti then singl e else e;
val case1 = Syntax.const @{syntax_const "_case1"} $ Term_Position.strip_positions p $ e;
val case2 =
--- a/src/HOL/Nominal/nominal_datatype.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Thu Jun 09 16:34:49 2011 +0200
@@ -622,7 +622,7 @@
(resolve_tac rep_intrs 1)) thy |> (fn ((_, r), thy) =>
let
val permT = mk_permT
- (TFree (Name.variant (map fst tvs) "'a", HOLogic.typeS));
+ (TFree (singleton (Name.variant_list (map fst tvs)) "'a", HOLogic.typeS));
val pi = Free ("pi", permT);
val T = Type (Sign.intern_type thy name, map TFree tvs);
in apfst (pair r o hd)
@@ -1169,7 +1169,7 @@
val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
val frees = tnames ~~ Ts;
val frees' = partition_cargs idxs frees;
- val z = (Name.variant tnames "z", fsT);
+ val z = (singleton (Name.variant_list tnames) "z", fsT);
fun mk_prem ((dt, s), T) =
let
--- a/src/HOL/Nominal/nominal_primrec.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Thu Jun 09 16:34:49 2011 +0200
@@ -207,7 +207,7 @@
fun make_def ctxt fixes fs (fname, ls, rs, rec_name, tname) =
let
val used = map fst (fold Term.add_frees fs []);
- val x = (Name.variant used "x", dummyT);
+ val x = (singleton (Name.variant_list used) "x", dummyT);
val frees = ls @ x :: rs;
val raw_rhs = list_abs_free (frees,
list_comb (Const (rec_name, dummyT), fs @ [Free x]))
--- a/src/HOL/Statespace/state_space.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Statespace/state_space.ML Thu Jun 09 16:34:49 2011 +0200
@@ -379,8 +379,8 @@
val Ts = distinct_types (map snd all_comps);
val arg_names = map fst args;
- val valueN = Name.variant arg_names "'value";
- val nameN = Name.variant (valueN::arg_names) "'name";
+ val valueN = singleton (Name.variant_list arg_names) "'value";
+ val nameN = singleton (Name.variant_list (valueN :: arg_names)) "'name";
val valueT = TFree (valueN, Sign.defaultS thy);
val nameT = TFree (nameN, Sign.defaultS thy);
val stateT = nameT --> valueT;
--- a/src/HOL/Tools/ATP/atp_translate.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Jun 09 16:34:49 2011 +0200
@@ -849,7 +849,7 @@
|>> (introduce_proxies format type_sys #> AAtom)
||> union (op =) atomic_types
fun do_quant bs q s T t' =
- let val s = Name.variant (map fst bs) s in
+ let val s = singleton (Name.variant_list (map fst bs)) s in
do_formula ((s, T) :: bs) t'
#>> mk_aquant q [(`make_bound_var s, SOME T)]
end
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Jun 09 16:34:49 2011 +0200
@@ -281,7 +281,7 @@
val recTs = Datatype_Aux.get_rec_types descr' sorts;
val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
val newTs = take (length (hd descr)) recTs;
- val T' = TFree (Name.variant used "'t", HOLogic.typeS);
+ val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' sorts dt) ---> T';
--- a/src/HOL/Tools/Datatype/datatype_case.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Thu Jun 09 16:34:49 2011 +0200
@@ -152,7 +152,7 @@
fun mk_case tab ctxt ty_match ty_inst type_of used range_ty =
let
- val name = Name.variant used "a";
+ val name = singleton (Name.variant_list used) "a";
fun expand constructors used ty ((_, []), _) =
raise CASE_ERROR ("mk_case: expand_var_row", ~1)
| expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) =
@@ -264,11 +264,12 @@
(* replace occurrences of dummy_pattern by distinct variables *)
(* internalize constant names *)
+ (* FIXME proper name context!? *)
fun prep_pat ((c as Const (@{syntax_const "_constrain"}, _)) $ t $ tT) used =
let val (t', used') = prep_pat t used
in (c $ t' $ tT, used') end
| prep_pat (Const (@{const_syntax dummy_pattern}, T)) used =
- let val x = Name.variant used "x"
+ let val x = singleton (Name.variant_list used) "x"
in (Free (x, T), x :: used) end
| prep_pat (Const (s, T)) used =
(Const (intern_const_syntax s, T), used)
@@ -305,6 +306,7 @@
(* destruct one level of pattern matching *)
+(* FIXME proper name context!? *)
fun gen_dest_case name_of type_of tab d used t =
(case apfst name_of (strip_comb t) of
(SOME cname, ts as _ :: _) =>
@@ -345,7 +347,7 @@
val R = type_of t;
val dummy =
if d then Const (@{const_name dummy_pattern}, R)
- else Free (Name.variant used "x", R);
+ else Free (singleton (Name.variant_list used) "x", R);
in
SOME (x,
map mk_case
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Jun 09 16:34:49 2011 +0200
@@ -47,7 +47,7 @@
|> Term.strip_comb
|> apsnd (fst o split_last)
|> list_comb;
- val lhs = Free (Name.variant params "case", Term.fastype_of rhs);
+ val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs);
val asm = (Thm.cterm_of thy o Logic.mk_equals) (lhs, rhs);
in
thms
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Thu Jun 09 16:34:49 2011 +0200
@@ -263,7 +263,7 @@
val recTs = Datatype_Aux.get_rec_types descr' sorts;
val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
val newTs = take (length (hd descr)) recTs;
- val T' = TFree (Name.variant used "'t", HOLogic.typeS);
+ val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
@@ -310,7 +310,7 @@
val recTs = Datatype_Aux.get_rec_types descr' sorts;
val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
val newTs = take (length (hd descr)) recTs;
- val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
+ val T' = TFree (singleton (Name.variant_list used') "'t", HOLogic.typeS);
val P = Free ("P", T' --> HOLogic.boolT);
fun make_split (((_, (_, _, constrs)), T), comb_t) =
--- a/src/HOL/Tools/Meson/meson_clausify.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu Jun 09 16:34:49 2011 +0200
@@ -75,7 +75,7 @@
in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
| dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
(*Universal quant: insert a free variable into body and continue*)
- let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
+ let val fname = singleton (Name.variant_list (OldTerm.add_term_names (p, []))) a
in dec_sko (subst_bound (Free(fname,T), p)) rhss end
| dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
| dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Jun 09 16:34:49 2011 +0200
@@ -205,7 +205,7 @@
(filter (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s)
(Symbol.explode name)))
val name'' = f (if name' = "" then empty else name')
- in (if member (op =) avoid name'' then Name.variant avoid name'' else name'') end
+ in if member (op =) avoid name'' then singleton (Name.variant_list avoid) name'' else name'' end
(** constant table **)
--- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML Thu Jun 09 16:34:49 2011 +0200
@@ -249,7 +249,7 @@
end
else
let
- val s = Name.variant names "x"
+ val s = singleton (Name.variant_list names) "x"
val v = Free (s, fastype_of t)
in
(v, (s :: names, HOLogic.mk_eq (v, t) :: eqs))
@@ -257,7 +257,7 @@
(*
if is_constrt thy t then (t, (names, eqs)) else
let
- val s = Name.variant names "x"
+ val s = singleton (Name.variant_list names) "x"
val v = Free (s, fastype_of t)
in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end;
*)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Jun 09 16:34:49 2011 +0200
@@ -906,7 +906,7 @@
val Type ("fun", [T, T']) = fastype_of comb;
val (Const (case_name, _), fs) = strip_comb comb
val used = Term.add_tfree_names comb []
- val U = TFree (Name.variant used "'t", HOLogic.typeS)
+ val U = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS)
val x = Free ("x", T)
val f = Free ("f", T' --> U)
fun apply_f f' =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Jun 09 16:34:49 2011 +0200
@@ -302,7 +302,7 @@
mk_random = (fn _ => error "no random generation"),
additional_arguments = fn names =>
let
- val depth_name = Name.variant names "depth"
+ val depth_name = singleton (Name.variant_list names) "depth"
in [Free (depth_name, @{typ code_numeral})] end,
modify_funT = (fn T => let val (Ts, U) = strip_type T
val Ts' = [@{typ code_numeral}] in (Ts @ Ts') ---> U end),
@@ -563,7 +563,7 @@
NONE => (Free (s, T), (names, (s, [])::vs))
| SOME xs =>
let
- val s' = Name.variant names s;
+ val s' = singleton (Name.variant_list names) s;
val v = Free (s', T)
in
(v, (s'::names, AList.update (op =) (s, v::xs) vs))
@@ -626,8 +626,8 @@
val eqs'' =
map (compile_arg compilation_modifiers additional_arguments ctxt param_modes) eqs''
val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
- val name = Name.variant names "x";
- val name' = Name.variant (name :: names) "y";
+ val name = singleton (Name.variant_list names) "x";
+ val name' = singleton (Name.variant_list (name :: names)) "y";
val T = HOLogic.mk_tupleT (map fastype_of out_ts);
val U = fastype_of success_t;
val U' = dest_predT compfuns U;
@@ -905,7 +905,7 @@
let
val (i, is) = argument_position_of mode position
val inp_var = nth_pair is (nth in_ts' i)
- val x = Name.variant all_vs "x"
+ val x = singleton (Name.variant_list all_vs) "x"
val xt = Free (x, fastype_of inp_var)
fun compile_single_case ((c, T), switched) =
let
@@ -962,7 +962,7 @@
(Free (hd param_vs, T), (tl param_vs, names))
else
let
- val new = Name.variant names "x"
+ val new = singleton (Name.variant_list names) "x"
in (Free (new, T), (param_vs, new :: names)) end)) inpTs
(param_vs, (all_vs @ param_vs))
val in_ts' = map_filter (map_filter_prod
@@ -1009,7 +1009,7 @@
fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name Product_Type.prod}, [T1, T2])) names =
if eq_mode (m, Input) orelse eq_mode (m, Output) then
let
- val x = Name.variant names "x"
+ val x = singleton (Name.variant_list names) "x"
in
(Free (x, T), x :: names)
end
@@ -1023,7 +1023,7 @@
| mk_args is_eval ((m as Fun _), T) names =
let
val funT = funT_of PredicateCompFuns.compfuns m T
- val x = Name.variant names "x"
+ val x = singleton (Name.variant_list names) "x"
val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names)
val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args
val t = fold_rev HOLogic.tupled_lambda args (PredicateCompFuns.mk_Eval
@@ -1033,7 +1033,7 @@
end
| mk_args is_eval (_, T) names =
let
- val x = Name.variant names "x"
+ val x = singleton (Name.variant_list names) "x"
in
(Free (x, T), x :: names)
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Jun 09 16:34:49 2011 +0200
@@ -118,7 +118,7 @@
val absnames = Name.variant_list names (map fst vars)
val frees = map2 (curry Free) absnames (map snd vars)
val body' = subst_bounds (rev frees, body)
- val resname = Name.variant (absnames @ names) "res"
+ val resname = singleton (Name.variant_list (absnames @ names)) "res"
val resvar = Free (resname, fastype_of body)
val t = flatten' body' ([], [])
|> map (fn (res, (inner_names, inner_prems)) =>
@@ -241,7 +241,7 @@
HOLogic.mk_eq (@{term False}, Bound 0)))
end
val argvs' = map2 lift_arg Ts argvs
- val resname = Name.variant names' "res"
+ val resname = singleton (Name.variant_list names') "res"
val resvar = Free (resname, body_type (fastype_of t))
val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs' @ [resvar]))
in (resvar, (resname :: names', prem :: prems')) end))
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Jun 09 16:34:49 2011 +0200
@@ -77,7 +77,7 @@
if is_compound atom then
let
val atom = Envir.beta_norm (Pattern.eta_long [] atom)
- val constname = Name.variant (map (Long_Name.base_name o fst) defs)
+ val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
((Long_Name.base_name constname) ^ "_aux")
val full_constname = Sign.full_bname thy constname
val (params, args) = List.partition (is_predT o fastype_of)
@@ -108,7 +108,7 @@
| SOME (atom', srs) =>
let
val frees = map Free (Term.add_frees atom' [])
- val constname = Name.variant (map (Long_Name.base_name o fst) defs)
+ val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
((Long_Name.base_name constname) ^ "_aux")
val full_constname = Sign.full_bname thy constname
val constT = map fastype_of frees ---> HOLogic.boolT
@@ -239,8 +239,9 @@
val vars = map Var (Term.add_vars abs_arg [])
val abs_arg' = Logic.unvarify_global abs_arg
val frees = map Free (Term.add_frees abs_arg' [])
- val constname = Name.variant (map (Long_Name.base_name o fst) new_defs)
- ((Long_Name.base_name constname) ^ "_hoaux")
+ val constname =
+ singleton (Name.variant_list (map (Long_Name.base_name o fst) new_defs))
+ ((Long_Name.base_name constname) ^ "_hoaux")
val full_constname = Sign.full_bname thy constname
val constT = map fastype_of frees ---> (fastype_of abs_arg')
val const = Const (full_constname, constT)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Thu Jun 09 16:34:49 2011 +0200
@@ -73,7 +73,8 @@
fun mk_fresh_name names =
let
val name =
- Name.variant names ("specialised_" ^ Long_Name.base_name (fst (dest_Const pred)))
+ singleton (Name.variant_list names)
+ ("specialised_" ^ Long_Name.base_name (fst (dest_Const pred)))
val bname = Sign.full_bname thy name
in
if Sign.declared_const thy bname then
@@ -119,7 +120,7 @@
val add_vars = fold_aterms (fn Var v => cons v | _ => I);
fun fresh_free T free_names =
let
- val free_name = Name.variant free_names "x"
+ val free_name = singleton (Name.variant_list free_names) "x"
in
(Free (free_name, T), free_name :: free_names)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Jun 09 16:34:49 2011 +0200
@@ -155,7 +155,7 @@
fun close_form t =
(t, [] |> Term.add_free_names t |> maps all_prefixes_of)
|> fold (fn ((s, i), T) => fn (t', taken) =>
- let val s' = Name.variant taken s in
+ let val s' = singleton (Name.variant_list taken) s in
((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
else Term.all) T
$ Abs (s', T, abstract_over (Var ((s, i), T), t')),
--- a/src/HOL/Tools/TFL/tfl.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Thu Jun 09 16:34:49 2011 +0200
@@ -324,7 +324,7 @@
map_index (fn (i, t) => (t,(i,true))) R)
val names = List.foldr OldTerm.add_term_names [] R
val atype = type_of(hd pats)
- and aname = Name.variant names "a"
+ and aname = singleton (Name.variant_list names) "a"
val a = Free(aname,atype)
val ty_info = Thry.match_info thy
val ty_match = Thry.match_type thy
@@ -480,7 +480,7 @@
val tych = Thry.typecheck thy
val WFREC_THM0 = Rules.ISPEC (tych functional) Thms.WFREC_COROLLARY
val Const(@{const_name All},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
- val R = Free (Name.variant (List.foldr OldTerm.add_term_names [] eqns) Rname,
+ val R = Free (singleton (Name.variant_list (List.foldr OldTerm.add_term_names [] eqns)) Rname,
Rtype)
val WFREC_THM = Rules.ISPECL [tych R, tych g] WFREC_THM0
val ([proto_def, WFR],_) = USyntax.strip_imp(concl WFREC_THM)
@@ -679,8 +679,8 @@
in fn pats =>
let val names = List.foldr OldTerm.add_term_names [] pats
val T = type_of (hd pats)
- val aname = Name.variant names "a"
- val vname = Name.variant (aname::names) "v"
+ val aname = singleton (Name.variant_list names) "a"
+ val vname = singleton (Name.variant_list (aname::names)) "v"
val a = Free (aname, T)
val v = Free (vname, T)
val a_eq_v = HOLogic.mk_eq(a,v)
@@ -830,8 +830,8 @@
val (pats,TCsl) = ListPair.unzip pat_TCs_list
val case_thm = complete_cases thy pats
val domain = (type_of o hd) pats
- val Pname = Name.variant (List.foldr (Library.foldr OldTerm.add_term_names)
- [] (pats::TCsl)) "P"
+ val Pname = singleton (Name.variant_list (List.foldr (Library.foldr OldTerm.add_term_names)
+ [] (pats::TCsl))) "P"
val P = Free(Pname, domain --> HOLogic.boolT)
val Sinduct = Rules.SPEC (tych P) Sinduction
val Sinduct_assumf = USyntax.rand ((#ant o USyntax.dest_imp o concl) Sinduct)
@@ -841,9 +841,10 @@
val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
val tasks = Utils.zip3 cases TCl' (Rules.CONJUNCTS Rinduct_assum)
val proved_cases = map (prove_case fconst thy) tasks
- val v = Free (Name.variant (List.foldr OldTerm.add_term_names [] (map concl proved_cases))
- "v",
- domain)
+ val v =
+ Free (singleton
+ (Name.variant_list (List.foldr OldTerm.add_term_names [] (map concl proved_cases))) "v",
+ domain)
val vtyped = tych v
val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS[th]th')
--- a/src/HOL/Tools/TFL/usyntax.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML Thu Jun 09 16:34:49 2011 +0200
@@ -238,7 +238,7 @@
fun dest_abs used (a as Abs(s, ty, M)) =
let
- val s' = Name.variant used s;
+ val s' = singleton (Name.variant_list used) s;
val v = Free(s', ty);
in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used)
end
--- a/src/HOL/Tools/inductive_codegen.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Thu Jun 09 16:34:49 2011 +0200
@@ -326,7 +326,7 @@
(case AList.lookup (op =) vs s of
NONE => (s, (names, (s, [s])::vs))
| SOME xs =>
- let val s' = Name.variant names s
+ let val s' = singleton (Name.variant_list names) s
in (s', (s'::names, AList.update (op =) (s, s'::xs) vs)) end);
fun distinct_v (Var ((s, 0), T)) nvs =
@@ -414,7 +414,7 @@
fun check_constrt t (names, eqs) =
if is_constrt thy t then (t, (names, eqs))
else
- let val s = Name.variant names "x";
+ let val s = singleton (Name.variant_list names) "x";
in (Var ((s, 0), fastype_of t), (s::names, (s, t)::eqs)) end;
fun compile_eq (s, t) gr =
--- a/src/HOL/Tools/inductive_realizer.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Thu Jun 09 16:34:49 2011 +0200
@@ -36,7 +36,7 @@
fun strip_all' used names (Const ("all", _) $ Abs (s, T, t)) =
let val (s', names') = (case names of
- [] => (Name.variant used s, [])
+ [] => (singleton (Name.variant_list used) s, [])
| name :: names' => (name, names'))
in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end
| strip_all' used names ((t as Const ("==>", _) $ P) $ Q) =
@@ -246,7 +246,7 @@
handle Datatype_Aux.Datatype_Empty name' =>
let
val name = Long_Name.base_name name';
- val dname = Name.variant used "Dummy";
+ val dname = singleton (Name.variant_list used) "Dummy";
in
thy
|> add_dummies f (map (add_dummy (Binding.name name) (Binding.name dname)) dts) (dname :: used)
--- a/src/HOL/Tools/record.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/record.ML Thu Jun 09 16:34:49 2011 +0200
@@ -1662,7 +1662,7 @@
val variants = map (fn Free (x, _) => x) vars_more;
val ext = mk_ext vars_more;
val s = Free (rN, extT);
- val P = Free (Name.variant variants "P", extT --> HOLogic.boolT);
+ val P = Free (singleton (Name.variant_list variants) "P", extT --> HOLogic.boolT);
val inject_prop =
let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
@@ -1677,7 +1677,7 @@
(All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
val split_meta_prop =
- let val P = Free (Name.variant variants "P", extT --> Term.propT) in
+ let val P = Free (singleton (Name.variant_list variants) "P", extT --> Term.propT) in
Logic.mk_equals
(All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
end;
@@ -1938,7 +1938,7 @@
val all_vars = parent_vars @ vars;
val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
- val zeta = (Name.variant (map #1 alphas) "'z", HOLogic.typeS);
+ val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", HOLogic.typeS);
val moreT = TFree zeta;
val more = Free (moreN, moreT);
val full_moreN = full (Binding.name moreN);
@@ -2134,9 +2134,9 @@
(* prepare propositions *)
val _ = timing_msg "record preparing propositions";
- val P = Free (Name.variant all_variants "P", rec_schemeT0 --> HOLogic.boolT);
- val C = Free (Name.variant all_variants "C", HOLogic.boolT);
- val P_unit = Free (Name.variant all_variants "P", recT0 --> HOLogic.boolT);
+ val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> HOLogic.boolT);
+ val C = Free (singleton (Name.variant_list all_variants) "C", HOLogic.boolT);
+ val P_unit = Free (singleton (Name.variant_list all_variants) "P", recT0 --> HOLogic.boolT);
(*selectors*)
val sel_conv_props =
@@ -2145,7 +2145,8 @@
(*updates*)
fun mk_upd_prop i (c, T) =
let
- val x' = Free (Name.variant all_variants (Long_Name.base_name c ^ "'"), T --> T);
+ val x' =
+ Free (singleton (Name.variant_list all_variants) (Long_Name.base_name c ^ "'"), T --> T);
val n = parent_fields_len + i;
val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more;
in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
@@ -2174,7 +2175,9 @@
(*split*)
val split_meta_prop =
- let val P = Free (Name.variant all_variants "P", rec_schemeT0-->Term.propT) in
+ let
+ val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0-->Term.propT);
+ in
Logic.mk_equals
(All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
end;
--- a/src/Pure/Isar/obtain.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Pure/Isar/obtain.ML Thu Jun 09 16:34:49 2011 +0200
@@ -133,7 +133,7 @@
val _ = Variable.warn_extra_tfrees fix_ctxt parms_ctxt;
(*obtain statements*)
- val thesisN = Name.variant xs Auto_Bind.thesisN;
+ val thesisN = singleton (Name.variant_list xs) Auto_Bind.thesisN;
val (thesis_var, thesis) = #1 (bind_judgment fix_ctxt thesisN);
val that_name = if name = "" then thatN else name;
--- a/src/Pure/codegen.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Pure/codegen.ML Thu Jun 09 16:34:49 2011 +0200
@@ -273,7 +273,7 @@
fun preprocess_term thy t =
let
- val x = Free (Name.variant (OldTerm.add_term_names (t, [])) "x", fastype_of t);
+ val x = Free (singleton (Name.variant_list (OldTerm.add_term_names (t, []))) "x", fastype_of t);
(* fake definition *)
val eq = Skip_Proof.make_thm thy (Logic.mk_equals (x, t));
fun err () = error "preprocess_term: bad preprocessor"
--- a/src/Pure/drule.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Pure/drule.ML Thu Jun 09 16:34:49 2011 +0200
@@ -337,7 +337,7 @@
[] => (fth, fn x => x)
| vars =>
let fun newName (Var(ix,_), (pairs,used)) =
- let val v = Name.variant used (string_of_indexname ix)
+ let val v = singleton (Name.variant_list used) (string_of_indexname ix)
in ((ix,v)::pairs, v::used) end;
val (alist, _) = List.foldr newName ([], Library.foldr OldTerm.add_term_names
(prop :: Thm.terms_of_tpairs tpairs, [])) vars
--- a/src/Pure/name.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Pure/name.ML Thu Jun 09 16:34:49 2011 +0200
@@ -26,7 +26,6 @@
val invent_list: string list -> string -> int -> string list
val variants: string list -> context -> string list * context
val variant_list: string list -> string list -> string list
- val variant: string list -> string -> string
val desymbolize: bool -> string -> string
end;
@@ -137,7 +136,6 @@
in (x' ^ replicate_string n "_", ctxt') end);
fun variant_list used names = #1 (make_context used |> variants names);
-fun variant used = singleton (variant_list used);
(* names conforming to typical requirements of identifiers in the world outside *)
--- a/src/Pure/proofterm.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Pure/proofterm.ML Thu Jun 09 16:34:49 2011 +0200
@@ -668,7 +668,7 @@
local
fun new_name (ix, (pairs,used)) =
- let val v = Name.variant used (string_of_indexname ix)
+ let val v = singleton (Name.variant_list used) (string_of_indexname ix)
in ((ix, v) :: pairs, v :: used) end;
fun freeze_one alist (ix, sort) = (case AList.lookup (op =) alist ix of
--- a/src/Pure/term.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Pure/term.ML Thu Jun 09 16:34:49 2011 +0200
@@ -936,7 +936,8 @@
| name_clash (Abs (_, _, t)) = name_clash t
| name_clash _ = false;
in
- if name_clash body then dest_abs (Name.variant [x] x, T, body) (*potentially slow*)
+ if name_clash body then
+ dest_abs (singleton (Name.variant_list [x]) x, T, body) (*potentially slow*)
else (x, subst_bound (Free (x, T), body))
end;
--- a/src/Pure/type.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Pure/type.ML Thu Jun 09 16:34:49 2011 +0200
@@ -358,7 +358,7 @@
local
fun new_name (ix, (pairs, used)) =
- let val v = Name.variant used (string_of_indexname ix)
+ let val v = singleton (Name.variant_list used) (string_of_indexname ix)
in ((ix, v) :: pairs, v :: used) end;
fun freeze_one alist (ix, sort) =
--- a/src/Tools/Code/code_printer.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Tools/Code/code_printer.ML Thu Jun 09 16:34:49 2011 +0200
@@ -184,7 +184,7 @@
fun fillup_param _ (_, SOME v) = v
| fillup_param x (i, NONE) = x ^ string_of_int i;
val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE);
- val x = Name.variant (map_filter I fished1) "x";
+ val x = singleton (Name.variant_list (map_filter I fished1)) "x";
val fished2 = map_index (fillup_param x) fished1;
val (fished3, _) = Name.variants fished2 Name.context;
val vars' = intro_vars fished3 vars;
--- a/src/Tools/Code/code_target.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Tools/Code/code_target.ML Thu Jun 09 16:34:49 2011 +0200
@@ -416,7 +416,7 @@
let
val _ = if Code_Thingol.contains_dict_var t then
error "Term to be evaluated contains free dictionaries" else ();
- val v' = Name.variant (map fst vs) "a";
+ val v' = singleton (Name.variant_list (map fst vs)) "a";
val vs' = (v', []) :: vs;
val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty];
val value_name = "Value.value.value"
--- a/src/Tools/IsaPlanner/isand.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Tools/IsaPlanner/isand.ML Thu Jun 09 16:34:49 2011 +0200
@@ -190,7 +190,7 @@
val tvars = List.foldr OldTerm.add_term_tvars [] ts;
val (names',renamings) =
List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) =>
- let val n2 = Name.variant Ns n in
+ let val n2 = singleton (Name.variant_list Ns) n in
(n2::Ns, (tv, (n2,s))::Rs)
end) (tfree_names @ names,[]) tvars;
in renamings end;
@@ -223,7 +223,7 @@
val Ns = List.foldr OldTerm.add_term_names names ts;
val (_,renamings) =
Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) =>
- let val n2 = Name.variant Ns n in
+ let val n2 = singleton (Name.variant_list Ns) n in
(n2 :: Ns, (v, (n2,ty)) :: Rs)
end) ((Ns,[]), vars);
in renamings end;
--- a/src/Tools/IsaPlanner/rw_inst.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML Thu Jun 09 16:34:49 2011 +0200
@@ -101,7 +101,7 @@
val names = usednames_of_thm rule;
val (fromnames,tonames,names2,Ts') =
Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) =>
- let val n2 = Name.variant names n in
+ let val n2 = singleton (Name.variant_list names) n in
(ctermify (Free(faken,ty)) :: rnf,
ctermify (Free(n2,ty)) :: rnt,
n2 :: names,
@@ -146,7 +146,7 @@
val vars_to_fix = union (op =) termvars cond_vs;
val (renamings, names2) =
List.foldr (fn (((n,i),ty), (vs, names')) =>
- let val n' = Name.variant names' n in
+ let val n' = singleton (Name.variant_list names') n in
((((n,i),ty), Free (n', ty)) :: vs, n'::names')
end)
([], names) vars_to_fix;
@@ -154,7 +154,7 @@
(* make a new fresh typefree instantiation for the given tvar *)
fun new_tfree (tv as (ix,sort), (pairs,used)) =
- let val v = Name.variant used (string_of_indexname ix)
+ let val v = singleton (Name.variant_list used) (string_of_indexname ix)
in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end;
--- a/src/Tools/eqsubst.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Tools/eqsubst.ML Thu Jun 09 16:34:49 2011 +0200
@@ -179,7 +179,7 @@
fun fakefree_badbounds Ts t =
let val (FakeTs,Ts,newnames) =
List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) =>
- let val newname = Name.variant usednames n
+ let val newname = singleton (Name.variant_list usednames) n
in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
(newname,ty)::Ts,
newname::usednames) end)
--- a/src/ZF/Tools/inductive_package.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/ZF/Tools/inductive_package.ML Thu Jun 09 16:34:49 2011 +0200
@@ -96,7 +96,7 @@
Syntax.string_of_term ctxt t);
(*** Construct the fixedpoint definition ***)
- val mk_variant = Name.variant (List.foldr OldTerm.add_term_names [] intr_tms);
+ val mk_variant = singleton (Name.variant_list (List.foldr OldTerm.add_term_names [] intr_tms));
val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
--- a/src/ZF/Tools/primrec_package.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/ZF/Tools/primrec_package.ML Thu Jun 09 16:34:49 2011 +0200
@@ -139,8 +139,9 @@
(** make definition **)
(*the recursive argument*)
- val rec_arg = Free (Name.variant (map #1 (ls@rs)) (Long_Name.base_name big_rec_name),
- Ind_Syntax.iT)
+ val rec_arg =
+ Free (singleton (Name.variant_list (map #1 (ls@rs))) (Long_Name.base_name big_rec_name),
+ Ind_Syntax.iT)
val def_tm = Logic.mk_equals
(subst_bound (rec_arg, fabs),