1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Thu Jun 09 15:38:49 2011 +0200
1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Thu Jun 09 16:34:49 2011 +0200
1.3 @@ -403,7 +403,7 @@
1.4
1.5 (* calculate function arguments of case combinator *)
1.6 val tns = map fst (Term.add_tfreesT lhsT [])
1.7 - val resultT = TFree (Name.variant tns "'t", @{sort pcpo})
1.8 + val resultT = TFree (singleton (Name.variant_list tns) "'t", @{sort pcpo})
1.9 fun fTs T = map (fn (_, args) => map snd args -->> T) spec
1.10 val fns = Datatype_Prop.indexify_names (map (K "f") spec)
1.11 val fs = map Free (fns ~~ fTs resultT)
1.12 @@ -768,7 +768,7 @@
1.13 val resultT : typ =
1.14 let
1.15 val ts : string list = map fst (Term.add_tfreesT lhsT [])
1.16 - val t : string = Name.variant ts "'t"
1.17 + val t : string = singleton (Name.variant_list ts) "'t"
1.18 in TFree (t, @{sort pcpo}) end
1.19
1.20 (* define match combinators *)
2.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML Thu Jun 09 15:38:49 2011 +0200
2.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML Thu Jun 09 16:34:49 2011 +0200
2.3 @@ -234,7 +234,7 @@
2.4 in comp_con T f rhs' (v::vs) taken' end
2.5 | Const (c, cT) =>
2.6 let
2.7 - val n = Name.variant taken "v"
2.8 + val n = singleton (Name.variant_list taken) "v"
2.9 val v = Free(n, T)
2.10 val m = Const(match_name c, matcherT (cT, fastype_of rhs))
2.11 val k = big_lambdas vs rhs
3.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy Thu Jun 09 15:38:49 2011 +0200
3.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Thu Jun 09 16:34:49 2011 +0200
3.3 @@ -531,7 +531,7 @@
3.4 (* prove strictness and reduction rules of pattern combinators *)
3.5 local
3.6 val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
3.7 - val rn = Name.variant tns "'r";
3.8 + val rn = singleton (Name.variant_list tns) "'r";
3.9 val R = TFree (rn, @{sort pcpo});
3.10 fun pat_lhs (pat, args) =
3.11 let
4.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Jun 09 15:38:49 2011 +0200
4.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Jun 09 16:34:49 2011 +0200
4.3 @@ -618,7 +618,6 @@
4.4 open Code_Thingol;
4.5
4.6 fun imp_program naming =
4.7 -
4.8 let
4.9 fun is_const c = case lookup_const naming c
4.10 of SOME c' => (fn c'' => c' = c'')
4.11 @@ -635,7 +634,7 @@
4.12 | dest_abs (t, ty) =
4.13 let
4.14 val vs = fold_varnames cons t [];
4.15 - val v = Name.variant vs "x";
4.16 + val v = singleton (Name.variant_list vs) "x";
4.17 val ty' = (hd o fst o unfold_fun) ty;
4.18 in ((SOME v, ty'), t `$ IVar (SOME v)) end;
4.19 fun force (t as IConst (c, _) `$ t') = if is_return c
5.1 --- a/src/HOL/Import/hol4rews.ML Thu Jun 09 15:38:49 2011 +0200
5.2 +++ b/src/HOL/Import/hol4rews.ML Thu Jun 09 16:34:49 2011 +0200
5.3 @@ -605,7 +605,7 @@
5.4 then F defname (* name_def *)
5.5 else if not (member (op =) used pdefname)
5.6 then F pdefname (* name_primdef *)
5.7 - else F (Name.variant used pdefname) (* last resort *)
5.8 + else F (singleton (Name.variant_list used) pdefname) (* last resort *)
5.9 end
5.10 end
5.11
6.1 --- a/src/HOL/Import/shuffler.ML Thu Jun 09 15:38:49 2011 +0200
6.2 +++ b/src/HOL/Import/shuffler.ML Thu Jun 09 16:34:49 2011 +0200
6.3 @@ -228,7 +228,7 @@
6.4 val (type_inst,_) =
6.5 fold (fn (w as (v,_), S) => fn (inst, used) =>
6.6 let
6.7 - val v' = Name.variant used v
6.8 + val v' = singleton (Name.variant_list used) v
6.9 in
6.10 ((w,TFree(v',S))::inst,v'::used)
6.11 end)
6.12 @@ -298,7 +298,7 @@
6.13 then
6.14 let
6.15 val cert = cterm_of thy
6.16 - val v = Free (Name.variant (Term.add_free_names t []) "v", xT)
6.17 + val v = Free (singleton (Name.variant_list (Term.add_free_names t [])) "v", xT)
6.18 val cv = cert v
6.19 val ct = cert t
6.20 val th = (Thm.assume ct)
6.21 @@ -361,7 +361,7 @@
6.22 Type("fun",[aT,bT]) =>
6.23 let
6.24 val cert = cterm_of thy
6.25 - val vname = Name.variant (Term.add_free_names t []) "v"
6.26 + val vname = singleton (Name.variant_list (Term.add_free_names t [])) "v"
6.27 val v = Free(vname,aT)
6.28 val cv = cert v
6.29 val ct = cert t
7.1 --- a/src/HOL/Inductive.thy Thu Jun 09 15:38:49 2011 +0200
7.2 +++ b/src/HOL/Inductive.thy Thu Jun 09 16:34:49 2011 +0200
7.3 @@ -295,7 +295,8 @@
7.4 let
7.5 fun fun_tr ctxt [cs] =
7.6 let
7.7 - val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
7.8 + (* FIXME proper name context!? *)
7.9 + val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT);
7.10 val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr ctxt [x, cs];
7.11 in lambda x ft end
7.12 in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
8.1 --- a/src/HOL/Library/Efficient_Nat.thy Thu Jun 09 15:38:49 2011 +0200
8.2 +++ b/src/HOL/Library/Efficient_Nat.thy Thu Jun 09 16:34:49 2011 +0200
8.3 @@ -113,8 +113,8 @@
8.4
8.5 fun remove_suc thy thms =
8.6 let
8.7 - val vname = Name.variant (map fst
8.8 - (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "n";
8.9 + val vname = singleton (Name.variant_list (map fst
8.10 + (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
8.11 val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
8.12 fun lhs_of th = snd (Thm.dest_comb
8.13 (fst (Thm.dest_comb (cprop_of th))));
8.14 @@ -166,8 +166,8 @@
8.15
8.16 fun remove_suc_clause thy thms =
8.17 let
8.18 - val vname = Name.variant (map fst
8.19 - (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
8.20 + val vname = singleton (Name.variant_list (map fst
8.21 + (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "x";
8.22 fun find_var (t as Const (@{const_name Suc}, _) $ (v as Var _)) = SOME (t, v)
8.23 | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
8.24 | find_var _ = NONE;
9.1 --- a/src/HOL/List.thy Thu Jun 09 15:38:49 2011 +0200
9.2 +++ b/src/HOL/List.thy Thu Jun 09 16:34:49 2011 +0200
9.3 @@ -383,7 +383,8 @@
9.4
9.5 fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
9.6 let
9.7 - val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
9.8 + (* FIXME proper name context!? *)
9.9 + val x = Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);
9.10 val e = if opti then singl e else e;
9.11 val case1 = Syntax.const @{syntax_const "_case1"} $ Term_Position.strip_positions p $ e;
9.12 val case2 =
10.1 --- a/src/HOL/Nominal/nominal_datatype.ML Thu Jun 09 15:38:49 2011 +0200
10.2 +++ b/src/HOL/Nominal/nominal_datatype.ML Thu Jun 09 16:34:49 2011 +0200
10.3 @@ -622,7 +622,7 @@
10.4 (resolve_tac rep_intrs 1)) thy |> (fn ((_, r), thy) =>
10.5 let
10.6 val permT = mk_permT
10.7 - (TFree (Name.variant (map fst tvs) "'a", HOLogic.typeS));
10.8 + (TFree (singleton (Name.variant_list (map fst tvs)) "'a", HOLogic.typeS));
10.9 val pi = Free ("pi", permT);
10.10 val T = Type (Sign.intern_type thy name, map TFree tvs);
10.11 in apfst (pair r o hd)
10.12 @@ -1169,7 +1169,7 @@
10.13 val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
10.14 val frees = tnames ~~ Ts;
10.15 val frees' = partition_cargs idxs frees;
10.16 - val z = (Name.variant tnames "z", fsT);
10.17 + val z = (singleton (Name.variant_list tnames) "z", fsT);
10.18
10.19 fun mk_prem ((dt, s), T) =
10.20 let
11.1 --- a/src/HOL/Nominal/nominal_primrec.ML Thu Jun 09 15:38:49 2011 +0200
11.2 +++ b/src/HOL/Nominal/nominal_primrec.ML Thu Jun 09 16:34:49 2011 +0200
11.3 @@ -207,7 +207,7 @@
11.4 fun make_def ctxt fixes fs (fname, ls, rs, rec_name, tname) =
11.5 let
11.6 val used = map fst (fold Term.add_frees fs []);
11.7 - val x = (Name.variant used "x", dummyT);
11.8 + val x = (singleton (Name.variant_list used) "x", dummyT);
11.9 val frees = ls @ x :: rs;
11.10 val raw_rhs = list_abs_free (frees,
11.11 list_comb (Const (rec_name, dummyT), fs @ [Free x]))
12.1 --- a/src/HOL/Statespace/state_space.ML Thu Jun 09 15:38:49 2011 +0200
12.2 +++ b/src/HOL/Statespace/state_space.ML Thu Jun 09 16:34:49 2011 +0200
12.3 @@ -379,8 +379,8 @@
12.4
12.5 val Ts = distinct_types (map snd all_comps);
12.6 val arg_names = map fst args;
12.7 - val valueN = Name.variant arg_names "'value";
12.8 - val nameN = Name.variant (valueN::arg_names) "'name";
12.9 + val valueN = singleton (Name.variant_list arg_names) "'value";
12.10 + val nameN = singleton (Name.variant_list (valueN :: arg_names)) "'name";
12.11 val valueT = TFree (valueN, Sign.defaultS thy);
12.12 val nameT = TFree (nameN, Sign.defaultS thy);
12.13 val stateT = nameT --> valueT;
13.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Thu Jun 09 15:38:49 2011 +0200
13.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Jun 09 16:34:49 2011 +0200
13.3 @@ -849,7 +849,7 @@
13.4 |>> (introduce_proxies format type_sys #> AAtom)
13.5 ||> union (op =) atomic_types
13.6 fun do_quant bs q s T t' =
13.7 - let val s = Name.variant (map fst bs) s in
13.8 + let val s = singleton (Name.variant_list (map fst bs)) s in
13.9 do_formula ((s, T) :: bs) t'
13.10 #>> mk_aquant q [(`make_bound_var s, SOME T)]
13.11 end
14.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Jun 09 15:38:49 2011 +0200
14.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Jun 09 16:34:49 2011 +0200
14.3 @@ -281,7 +281,7 @@
14.4 val recTs = Datatype_Aux.get_rec_types descr' sorts;
14.5 val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
14.6 val newTs = take (length (hd descr)) recTs;
14.7 - val T' = TFree (Name.variant used "'t", HOLogic.typeS);
14.8 + val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
14.9
14.10 fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' sorts dt) ---> T';
14.11
15.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML Thu Jun 09 15:38:49 2011 +0200
15.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Thu Jun 09 16:34:49 2011 +0200
15.3 @@ -152,7 +152,7 @@
15.4
15.5 fun mk_case tab ctxt ty_match ty_inst type_of used range_ty =
15.6 let
15.7 - val name = Name.variant used "a";
15.8 + val name = singleton (Name.variant_list used) "a";
15.9 fun expand constructors used ty ((_, []), _) =
15.10 raise CASE_ERROR ("mk_case: expand_var_row", ~1)
15.11 | expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) =
15.12 @@ -264,11 +264,12 @@
15.13
15.14 (* replace occurrences of dummy_pattern by distinct variables *)
15.15 (* internalize constant names *)
15.16 + (* FIXME proper name context!? *)
15.17 fun prep_pat ((c as Const (@{syntax_const "_constrain"}, _)) $ t $ tT) used =
15.18 let val (t', used') = prep_pat t used
15.19 in (c $ t' $ tT, used') end
15.20 | prep_pat (Const (@{const_syntax dummy_pattern}, T)) used =
15.21 - let val x = Name.variant used "x"
15.22 + let val x = singleton (Name.variant_list used) "x"
15.23 in (Free (x, T), x :: used) end
15.24 | prep_pat (Const (s, T)) used =
15.25 (Const (intern_const_syntax s, T), used)
15.26 @@ -305,6 +306,7 @@
15.27
15.28 (* destruct one level of pattern matching *)
15.29
15.30 +(* FIXME proper name context!? *)
15.31 fun gen_dest_case name_of type_of tab d used t =
15.32 (case apfst name_of (strip_comb t) of
15.33 (SOME cname, ts as _ :: _) =>
15.34 @@ -345,7 +347,7 @@
15.35 val R = type_of t;
15.36 val dummy =
15.37 if d then Const (@{const_name dummy_pattern}, R)
15.38 - else Free (Name.variant used "x", R);
15.39 + else Free (singleton (Name.variant_list used) "x", R);
15.40 in
15.41 SOME (x,
15.42 map mk_case
16.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Jun 09 15:38:49 2011 +0200
16.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Jun 09 16:34:49 2011 +0200
16.3 @@ -47,7 +47,7 @@
16.4 |> Term.strip_comb
16.5 |> apsnd (fst o split_last)
16.6 |> list_comb;
16.7 - val lhs = Free (Name.variant params "case", Term.fastype_of rhs);
16.8 + val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs);
16.9 val asm = (Thm.cterm_of thy o Logic.mk_equals) (lhs, rhs);
16.10 in
16.11 thms
17.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML Thu Jun 09 15:38:49 2011 +0200
17.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML Thu Jun 09 16:34:49 2011 +0200
17.3 @@ -263,7 +263,7 @@
17.4 val recTs = Datatype_Aux.get_rec_types descr' sorts;
17.5 val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
17.6 val newTs = take (length (hd descr)) recTs;
17.7 - val T' = TFree (Name.variant used "'t", HOLogic.typeS);
17.8 + val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
17.9
17.10 val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
17.11 map (fn (_, cargs) =>
17.12 @@ -310,7 +310,7 @@
17.13 val recTs = Datatype_Aux.get_rec_types descr' sorts;
17.14 val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
17.15 val newTs = take (length (hd descr)) recTs;
17.16 - val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
17.17 + val T' = TFree (singleton (Name.variant_list used') "'t", HOLogic.typeS);
17.18 val P = Free ("P", T' --> HOLogic.boolT);
17.19
17.20 fun make_split (((_, (_, _, constrs)), T), comb_t) =
18.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML Thu Jun 09 15:38:49 2011 +0200
18.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu Jun 09 16:34:49 2011 +0200
18.3 @@ -75,7 +75,7 @@
18.4 in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
18.5 | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
18.6 (*Universal quant: insert a free variable into body and continue*)
18.7 - let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
18.8 + let val fname = singleton (Name.variant_list (OldTerm.add_term_names (p, []))) a
18.9 in dec_sko (subst_bound (Free(fname,T), p)) rhss end
18.10 | dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
18.11 | dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
19.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Jun 09 15:38:49 2011 +0200
19.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Jun 09 16:34:49 2011 +0200
19.3 @@ -205,7 +205,7 @@
19.4 (filter (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s)
19.5 (Symbol.explode name)))
19.6 val name'' = f (if name' = "" then empty else name')
19.7 - in (if member (op =) avoid name'' then Name.variant avoid name'' else name'') end
19.8 + in if member (op =) avoid name'' then singleton (Name.variant_list avoid) name'' else name'' end
19.9
19.10 (** constant table **)
19.11
20.1 --- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML Thu Jun 09 15:38:49 2011 +0200
20.2 +++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML Thu Jun 09 16:34:49 2011 +0200
20.3 @@ -249,7 +249,7 @@
20.4 end
20.5 else
20.6 let
20.7 - val s = Name.variant names "x"
20.8 + val s = singleton (Name.variant_list names) "x"
20.9 val v = Free (s, fastype_of t)
20.10 in
20.11 (v, (s :: names, HOLogic.mk_eq (v, t) :: eqs))
20.12 @@ -257,7 +257,7 @@
20.13 (*
20.14 if is_constrt thy t then (t, (names, eqs)) else
20.15 let
20.16 - val s = Name.variant names "x"
20.17 + val s = singleton (Name.variant_list names) "x"
20.18 val v = Free (s, fastype_of t)
20.19 in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end;
20.20 *)
21.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Jun 09 15:38:49 2011 +0200
21.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Jun 09 16:34:49 2011 +0200
21.3 @@ -906,7 +906,7 @@
21.4 val Type ("fun", [T, T']) = fastype_of comb;
21.5 val (Const (case_name, _), fs) = strip_comb comb
21.6 val used = Term.add_tfree_names comb []
21.7 - val U = TFree (Name.variant used "'t", HOLogic.typeS)
21.8 + val U = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS)
21.9 val x = Free ("x", T)
21.10 val f = Free ("f", T' --> U)
21.11 fun apply_f f' =
22.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Jun 09 15:38:49 2011 +0200
22.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Jun 09 16:34:49 2011 +0200
22.3 @@ -302,7 +302,7 @@
22.4 mk_random = (fn _ => error "no random generation"),
22.5 additional_arguments = fn names =>
22.6 let
22.7 - val depth_name = Name.variant names "depth"
22.8 + val depth_name = singleton (Name.variant_list names) "depth"
22.9 in [Free (depth_name, @{typ code_numeral})] end,
22.10 modify_funT = (fn T => let val (Ts, U) = strip_type T
22.11 val Ts' = [@{typ code_numeral}] in (Ts @ Ts') ---> U end),
22.12 @@ -563,7 +563,7 @@
22.13 NONE => (Free (s, T), (names, (s, [])::vs))
22.14 | SOME xs =>
22.15 let
22.16 - val s' = Name.variant names s;
22.17 + val s' = singleton (Name.variant_list names) s;
22.18 val v = Free (s', T)
22.19 in
22.20 (v, (s'::names, AList.update (op =) (s, v::xs) vs))
22.21 @@ -626,8 +626,8 @@
22.22 val eqs'' =
22.23 map (compile_arg compilation_modifiers additional_arguments ctxt param_modes) eqs''
22.24 val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
22.25 - val name = Name.variant names "x";
22.26 - val name' = Name.variant (name :: names) "y";
22.27 + val name = singleton (Name.variant_list names) "x";
22.28 + val name' = singleton (Name.variant_list (name :: names)) "y";
22.29 val T = HOLogic.mk_tupleT (map fastype_of out_ts);
22.30 val U = fastype_of success_t;
22.31 val U' = dest_predT compfuns U;
22.32 @@ -905,7 +905,7 @@
22.33 let
22.34 val (i, is) = argument_position_of mode position
22.35 val inp_var = nth_pair is (nth in_ts' i)
22.36 - val x = Name.variant all_vs "x"
22.37 + val x = singleton (Name.variant_list all_vs) "x"
22.38 val xt = Free (x, fastype_of inp_var)
22.39 fun compile_single_case ((c, T), switched) =
22.40 let
22.41 @@ -962,7 +962,7 @@
22.42 (Free (hd param_vs, T), (tl param_vs, names))
22.43 else
22.44 let
22.45 - val new = Name.variant names "x"
22.46 + val new = singleton (Name.variant_list names) "x"
22.47 in (Free (new, T), (param_vs, new :: names)) end)) inpTs
22.48 (param_vs, (all_vs @ param_vs))
22.49 val in_ts' = map_filter (map_filter_prod
22.50 @@ -1009,7 +1009,7 @@
22.51 fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name Product_Type.prod}, [T1, T2])) names =
22.52 if eq_mode (m, Input) orelse eq_mode (m, Output) then
22.53 let
22.54 - val x = Name.variant names "x"
22.55 + val x = singleton (Name.variant_list names) "x"
22.56 in
22.57 (Free (x, T), x :: names)
22.58 end
22.59 @@ -1023,7 +1023,7 @@
22.60 | mk_args is_eval ((m as Fun _), T) names =
22.61 let
22.62 val funT = funT_of PredicateCompFuns.compfuns m T
22.63 - val x = Name.variant names "x"
22.64 + val x = singleton (Name.variant_list names) "x"
22.65 val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names)
22.66 val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args
22.67 val t = fold_rev HOLogic.tupled_lambda args (PredicateCompFuns.mk_Eval
22.68 @@ -1033,7 +1033,7 @@
22.69 end
22.70 | mk_args is_eval (_, T) names =
22.71 let
22.72 - val x = Name.variant names "x"
22.73 + val x = singleton (Name.variant_list names) "x"
22.74 in
22.75 (Free (x, T), x :: names)
22.76 end
23.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Jun 09 15:38:49 2011 +0200
23.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Jun 09 16:34:49 2011 +0200
23.3 @@ -118,7 +118,7 @@
23.4 val absnames = Name.variant_list names (map fst vars)
23.5 val frees = map2 (curry Free) absnames (map snd vars)
23.6 val body' = subst_bounds (rev frees, body)
23.7 - val resname = Name.variant (absnames @ names) "res"
23.8 + val resname = singleton (Name.variant_list (absnames @ names)) "res"
23.9 val resvar = Free (resname, fastype_of body)
23.10 val t = flatten' body' ([], [])
23.11 |> map (fn (res, (inner_names, inner_prems)) =>
23.12 @@ -241,7 +241,7 @@
23.13 HOLogic.mk_eq (@{term False}, Bound 0)))
23.14 end
23.15 val argvs' = map2 lift_arg Ts argvs
23.16 - val resname = Name.variant names' "res"
23.17 + val resname = singleton (Name.variant_list names') "res"
23.18 val resvar = Free (resname, body_type (fastype_of t))
23.19 val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs' @ [resvar]))
23.20 in (resvar, (resname :: names', prem :: prems')) end))
24.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Jun 09 15:38:49 2011 +0200
24.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Jun 09 16:34:49 2011 +0200
24.3 @@ -77,7 +77,7 @@
24.4 if is_compound atom then
24.5 let
24.6 val atom = Envir.beta_norm (Pattern.eta_long [] atom)
24.7 - val constname = Name.variant (map (Long_Name.base_name o fst) defs)
24.8 + val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
24.9 ((Long_Name.base_name constname) ^ "_aux")
24.10 val full_constname = Sign.full_bname thy constname
24.11 val (params, args) = List.partition (is_predT o fastype_of)
24.12 @@ -108,7 +108,7 @@
24.13 | SOME (atom', srs) =>
24.14 let
24.15 val frees = map Free (Term.add_frees atom' [])
24.16 - val constname = Name.variant (map (Long_Name.base_name o fst) defs)
24.17 + val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
24.18 ((Long_Name.base_name constname) ^ "_aux")
24.19 val full_constname = Sign.full_bname thy constname
24.20 val constT = map fastype_of frees ---> HOLogic.boolT
24.21 @@ -239,8 +239,9 @@
24.22 val vars = map Var (Term.add_vars abs_arg [])
24.23 val abs_arg' = Logic.unvarify_global abs_arg
24.24 val frees = map Free (Term.add_frees abs_arg' [])
24.25 - val constname = Name.variant (map (Long_Name.base_name o fst) new_defs)
24.26 - ((Long_Name.base_name constname) ^ "_hoaux")
24.27 + val constname =
24.28 + singleton (Name.variant_list (map (Long_Name.base_name o fst) new_defs))
24.29 + ((Long_Name.base_name constname) ^ "_hoaux")
24.30 val full_constname = Sign.full_bname thy constname
24.31 val constT = map fastype_of frees ---> (fastype_of abs_arg')
24.32 val const = Const (full_constname, constT)
25.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Thu Jun 09 15:38:49 2011 +0200
25.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Thu Jun 09 16:34:49 2011 +0200
25.3 @@ -73,7 +73,8 @@
25.4 fun mk_fresh_name names =
25.5 let
25.6 val name =
25.7 - Name.variant names ("specialised_" ^ Long_Name.base_name (fst (dest_Const pred)))
25.8 + singleton (Name.variant_list names)
25.9 + ("specialised_" ^ Long_Name.base_name (fst (dest_Const pred)))
25.10 val bname = Sign.full_bname thy name
25.11 in
25.12 if Sign.declared_const thy bname then
25.13 @@ -119,7 +120,7 @@
25.14 val add_vars = fold_aterms (fn Var v => cons v | _ => I);
25.15 fun fresh_free T free_names =
25.16 let
25.17 - val free_name = Name.variant free_names "x"
25.18 + val free_name = singleton (Name.variant_list free_names) "x"
25.19 in
25.20 (Free (free_name, T), free_name :: free_names)
25.21 end
26.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Jun 09 15:38:49 2011 +0200
26.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Jun 09 16:34:49 2011 +0200
26.3 @@ -155,7 +155,7 @@
26.4 fun close_form t =
26.5 (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
26.6 |> fold (fn ((s, i), T) => fn (t', taken) =>
26.7 - let val s' = Name.variant taken s in
26.8 + let val s' = singleton (Name.variant_list taken) s in
26.9 ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
26.10 else Term.all) T
26.11 $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
27.1 --- a/src/HOL/Tools/TFL/tfl.ML Thu Jun 09 15:38:49 2011 +0200
27.2 +++ b/src/HOL/Tools/TFL/tfl.ML Thu Jun 09 16:34:49 2011 +0200
27.3 @@ -324,7 +324,7 @@
27.4 map_index (fn (i, t) => (t,(i,true))) R)
27.5 val names = List.foldr OldTerm.add_term_names [] R
27.6 val atype = type_of(hd pats)
27.7 - and aname = Name.variant names "a"
27.8 + and aname = singleton (Name.variant_list names) "a"
27.9 val a = Free(aname,atype)
27.10 val ty_info = Thry.match_info thy
27.11 val ty_match = Thry.match_type thy
27.12 @@ -480,7 +480,7 @@
27.13 val tych = Thry.typecheck thy
27.14 val WFREC_THM0 = Rules.ISPEC (tych functional) Thms.WFREC_COROLLARY
27.15 val Const(@{const_name All},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
27.16 - val R = Free (Name.variant (List.foldr OldTerm.add_term_names [] eqns) Rname,
27.17 + val R = Free (singleton (Name.variant_list (List.foldr OldTerm.add_term_names [] eqns)) Rname,
27.18 Rtype)
27.19 val WFREC_THM = Rules.ISPECL [tych R, tych g] WFREC_THM0
27.20 val ([proto_def, WFR],_) = USyntax.strip_imp(concl WFREC_THM)
27.21 @@ -679,8 +679,8 @@
27.22 in fn pats =>
27.23 let val names = List.foldr OldTerm.add_term_names [] pats
27.24 val T = type_of (hd pats)
27.25 - val aname = Name.variant names "a"
27.26 - val vname = Name.variant (aname::names) "v"
27.27 + val aname = singleton (Name.variant_list names) "a"
27.28 + val vname = singleton (Name.variant_list (aname::names)) "v"
27.29 val a = Free (aname, T)
27.30 val v = Free (vname, T)
27.31 val a_eq_v = HOLogic.mk_eq(a,v)
27.32 @@ -830,8 +830,8 @@
27.33 val (pats,TCsl) = ListPair.unzip pat_TCs_list
27.34 val case_thm = complete_cases thy pats
27.35 val domain = (type_of o hd) pats
27.36 - val Pname = Name.variant (List.foldr (Library.foldr OldTerm.add_term_names)
27.37 - [] (pats::TCsl)) "P"
27.38 + val Pname = singleton (Name.variant_list (List.foldr (Library.foldr OldTerm.add_term_names)
27.39 + [] (pats::TCsl))) "P"
27.40 val P = Free(Pname, domain --> HOLogic.boolT)
27.41 val Sinduct = Rules.SPEC (tych P) Sinduction
27.42 val Sinduct_assumf = USyntax.rand ((#ant o USyntax.dest_imp o concl) Sinduct)
27.43 @@ -841,9 +841,10 @@
27.44 val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
27.45 val tasks = Utils.zip3 cases TCl' (Rules.CONJUNCTS Rinduct_assum)
27.46 val proved_cases = map (prove_case fconst thy) tasks
27.47 - val v = Free (Name.variant (List.foldr OldTerm.add_term_names [] (map concl proved_cases))
27.48 - "v",
27.49 - domain)
27.50 + val v =
27.51 + Free (singleton
27.52 + (Name.variant_list (List.foldr OldTerm.add_term_names [] (map concl proved_cases))) "v",
27.53 + domain)
27.54 val vtyped = tych v
27.55 val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
27.56 val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS[th]th')
28.1 --- a/src/HOL/Tools/TFL/usyntax.ML Thu Jun 09 15:38:49 2011 +0200
28.2 +++ b/src/HOL/Tools/TFL/usyntax.ML Thu Jun 09 16:34:49 2011 +0200
28.3 @@ -238,7 +238,7 @@
28.4
28.5 fun dest_abs used (a as Abs(s, ty, M)) =
28.6 let
28.7 - val s' = Name.variant used s;
28.8 + val s' = singleton (Name.variant_list used) s;
28.9 val v = Free(s', ty);
28.10 in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used)
28.11 end
29.1 --- a/src/HOL/Tools/inductive_codegen.ML Thu Jun 09 15:38:49 2011 +0200
29.2 +++ b/src/HOL/Tools/inductive_codegen.ML Thu Jun 09 16:34:49 2011 +0200
29.3 @@ -326,7 +326,7 @@
29.4 (case AList.lookup (op =) vs s of
29.5 NONE => (s, (names, (s, [s])::vs))
29.6 | SOME xs =>
29.7 - let val s' = Name.variant names s
29.8 + let val s' = singleton (Name.variant_list names) s
29.9 in (s', (s'::names, AList.update (op =) (s, s'::xs) vs)) end);
29.10
29.11 fun distinct_v (Var ((s, 0), T)) nvs =
29.12 @@ -414,7 +414,7 @@
29.13 fun check_constrt t (names, eqs) =
29.14 if is_constrt thy t then (t, (names, eqs))
29.15 else
29.16 - let val s = Name.variant names "x";
29.17 + let val s = singleton (Name.variant_list names) "x";
29.18 in (Var ((s, 0), fastype_of t), (s::names, (s, t)::eqs)) end;
29.19
29.20 fun compile_eq (s, t) gr =
30.1 --- a/src/HOL/Tools/inductive_realizer.ML Thu Jun 09 15:38:49 2011 +0200
30.2 +++ b/src/HOL/Tools/inductive_realizer.ML Thu Jun 09 16:34:49 2011 +0200
30.3 @@ -36,7 +36,7 @@
30.4
30.5 fun strip_all' used names (Const ("all", _) $ Abs (s, T, t)) =
30.6 let val (s', names') = (case names of
30.7 - [] => (Name.variant used s, [])
30.8 + [] => (singleton (Name.variant_list used) s, [])
30.9 | name :: names' => (name, names'))
30.10 in strip_all' (s'::used) names' (subst_bound (Free (s', T), t)) end
30.11 | strip_all' used names ((t as Const ("==>", _) $ P) $ Q) =
30.12 @@ -246,7 +246,7 @@
30.13 handle Datatype_Aux.Datatype_Empty name' =>
30.14 let
30.15 val name = Long_Name.base_name name';
30.16 - val dname = Name.variant used "Dummy";
30.17 + val dname = singleton (Name.variant_list used) "Dummy";
30.18 in
30.19 thy
30.20 |> add_dummies f (map (add_dummy (Binding.name name) (Binding.name dname)) dts) (dname :: used)
31.1 --- a/src/HOL/Tools/record.ML Thu Jun 09 15:38:49 2011 +0200
31.2 +++ b/src/HOL/Tools/record.ML Thu Jun 09 16:34:49 2011 +0200
31.3 @@ -1662,7 +1662,7 @@
31.4 val variants = map (fn Free (x, _) => x) vars_more;
31.5 val ext = mk_ext vars_more;
31.6 val s = Free (rN, extT);
31.7 - val P = Free (Name.variant variants "P", extT --> HOLogic.boolT);
31.8 + val P = Free (singleton (Name.variant_list variants) "P", extT --> HOLogic.boolT);
31.9
31.10 val inject_prop =
31.11 let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
31.12 @@ -1677,7 +1677,7 @@
31.13 (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
31.14
31.15 val split_meta_prop =
31.16 - let val P = Free (Name.variant variants "P", extT --> Term.propT) in
31.17 + let val P = Free (singleton (Name.variant_list variants) "P", extT --> Term.propT) in
31.18 Logic.mk_equals
31.19 (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
31.20 end;
31.21 @@ -1938,7 +1938,7 @@
31.22 val all_vars = parent_vars @ vars;
31.23 val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
31.24
31.25 - val zeta = (Name.variant (map #1 alphas) "'z", HOLogic.typeS);
31.26 + val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", HOLogic.typeS);
31.27 val moreT = TFree zeta;
31.28 val more = Free (moreN, moreT);
31.29 val full_moreN = full (Binding.name moreN);
31.30 @@ -2134,9 +2134,9 @@
31.31
31.32 (* prepare propositions *)
31.33 val _ = timing_msg "record preparing propositions";
31.34 - val P = Free (Name.variant all_variants "P", rec_schemeT0 --> HOLogic.boolT);
31.35 - val C = Free (Name.variant all_variants "C", HOLogic.boolT);
31.36 - val P_unit = Free (Name.variant all_variants "P", recT0 --> HOLogic.boolT);
31.37 + val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> HOLogic.boolT);
31.38 + val C = Free (singleton (Name.variant_list all_variants) "C", HOLogic.boolT);
31.39 + val P_unit = Free (singleton (Name.variant_list all_variants) "P", recT0 --> HOLogic.boolT);
31.40
31.41 (*selectors*)
31.42 val sel_conv_props =
31.43 @@ -2145,7 +2145,8 @@
31.44 (*updates*)
31.45 fun mk_upd_prop i (c, T) =
31.46 let
31.47 - val x' = Free (Name.variant all_variants (Long_Name.base_name c ^ "'"), T --> T);
31.48 + val x' =
31.49 + Free (singleton (Name.variant_list all_variants) (Long_Name.base_name c ^ "'"), T --> T);
31.50 val n = parent_fields_len + i;
31.51 val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more;
31.52 in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
31.53 @@ -2174,7 +2175,9 @@
31.54
31.55 (*split*)
31.56 val split_meta_prop =
31.57 - let val P = Free (Name.variant all_variants "P", rec_schemeT0-->Term.propT) in
31.58 + let
31.59 + val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0-->Term.propT);
31.60 + in
31.61 Logic.mk_equals
31.62 (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
31.63 end;
32.1 --- a/src/Pure/Isar/obtain.ML Thu Jun 09 15:38:49 2011 +0200
32.2 +++ b/src/Pure/Isar/obtain.ML Thu Jun 09 16:34:49 2011 +0200
32.3 @@ -133,7 +133,7 @@
32.4 val _ = Variable.warn_extra_tfrees fix_ctxt parms_ctxt;
32.5
32.6 (*obtain statements*)
32.7 - val thesisN = Name.variant xs Auto_Bind.thesisN;
32.8 + val thesisN = singleton (Name.variant_list xs) Auto_Bind.thesisN;
32.9 val (thesis_var, thesis) = #1 (bind_judgment fix_ctxt thesisN);
32.10
32.11 val that_name = if name = "" then thatN else name;
33.1 --- a/src/Pure/codegen.ML Thu Jun 09 15:38:49 2011 +0200
33.2 +++ b/src/Pure/codegen.ML Thu Jun 09 16:34:49 2011 +0200
33.3 @@ -273,7 +273,7 @@
33.4
33.5 fun preprocess_term thy t =
33.6 let
33.7 - val x = Free (Name.variant (OldTerm.add_term_names (t, [])) "x", fastype_of t);
33.8 + val x = Free (singleton (Name.variant_list (OldTerm.add_term_names (t, []))) "x", fastype_of t);
33.9 (* fake definition *)
33.10 val eq = Skip_Proof.make_thm thy (Logic.mk_equals (x, t));
33.11 fun err () = error "preprocess_term: bad preprocessor"
34.1 --- a/src/Pure/drule.ML Thu Jun 09 15:38:49 2011 +0200
34.2 +++ b/src/Pure/drule.ML Thu Jun 09 16:34:49 2011 +0200
34.3 @@ -337,7 +337,7 @@
34.4 [] => (fth, fn x => x)
34.5 | vars =>
34.6 let fun newName (Var(ix,_), (pairs,used)) =
34.7 - let val v = Name.variant used (string_of_indexname ix)
34.8 + let val v = singleton (Name.variant_list used) (string_of_indexname ix)
34.9 in ((ix,v)::pairs, v::used) end;
34.10 val (alist, _) = List.foldr newName ([], Library.foldr OldTerm.add_term_names
34.11 (prop :: Thm.terms_of_tpairs tpairs, [])) vars
35.1 --- a/src/Pure/name.ML Thu Jun 09 15:38:49 2011 +0200
35.2 +++ b/src/Pure/name.ML Thu Jun 09 16:34:49 2011 +0200
35.3 @@ -26,7 +26,6 @@
35.4 val invent_list: string list -> string -> int -> string list
35.5 val variants: string list -> context -> string list * context
35.6 val variant_list: string list -> string list -> string list
35.7 - val variant: string list -> string -> string
35.8 val desymbolize: bool -> string -> string
35.9 end;
35.10
35.11 @@ -137,7 +136,6 @@
35.12 in (x' ^ replicate_string n "_", ctxt') end);
35.13
35.14 fun variant_list used names = #1 (make_context used |> variants names);
35.15 -fun variant used = singleton (variant_list used);
35.16
35.17
35.18 (* names conforming to typical requirements of identifiers in the world outside *)
36.1 --- a/src/Pure/proofterm.ML Thu Jun 09 15:38:49 2011 +0200
36.2 +++ b/src/Pure/proofterm.ML Thu Jun 09 16:34:49 2011 +0200
36.3 @@ -668,7 +668,7 @@
36.4 local
36.5
36.6 fun new_name (ix, (pairs,used)) =
36.7 - let val v = Name.variant used (string_of_indexname ix)
36.8 + let val v = singleton (Name.variant_list used) (string_of_indexname ix)
36.9 in ((ix, v) :: pairs, v :: used) end;
36.10
36.11 fun freeze_one alist (ix, sort) = (case AList.lookup (op =) alist ix of
37.1 --- a/src/Pure/term.ML Thu Jun 09 15:38:49 2011 +0200
37.2 +++ b/src/Pure/term.ML Thu Jun 09 16:34:49 2011 +0200
37.3 @@ -936,7 +936,8 @@
37.4 | name_clash (Abs (_, _, t)) = name_clash t
37.5 | name_clash _ = false;
37.6 in
37.7 - if name_clash body then dest_abs (Name.variant [x] x, T, body) (*potentially slow*)
37.8 + if name_clash body then
37.9 + dest_abs (singleton (Name.variant_list [x]) x, T, body) (*potentially slow*)
37.10 else (x, subst_bound (Free (x, T), body))
37.11 end;
37.12
38.1 --- a/src/Pure/type.ML Thu Jun 09 15:38:49 2011 +0200
38.2 +++ b/src/Pure/type.ML Thu Jun 09 16:34:49 2011 +0200
38.3 @@ -358,7 +358,7 @@
38.4 local
38.5
38.6 fun new_name (ix, (pairs, used)) =
38.7 - let val v = Name.variant used (string_of_indexname ix)
38.8 + let val v = singleton (Name.variant_list used) (string_of_indexname ix)
38.9 in ((ix, v) :: pairs, v :: used) end;
38.10
38.11 fun freeze_one alist (ix, sort) =
39.1 --- a/src/Tools/Code/code_printer.ML Thu Jun 09 15:38:49 2011 +0200
39.2 +++ b/src/Tools/Code/code_printer.ML Thu Jun 09 16:34:49 2011 +0200
39.3 @@ -184,7 +184,7 @@
39.4 fun fillup_param _ (_, SOME v) = v
39.5 | fillup_param x (i, NONE) = x ^ string_of_int i;
39.6 val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE);
39.7 - val x = Name.variant (map_filter I fished1) "x";
39.8 + val x = singleton (Name.variant_list (map_filter I fished1)) "x";
39.9 val fished2 = map_index (fillup_param x) fished1;
39.10 val (fished3, _) = Name.variants fished2 Name.context;
39.11 val vars' = intro_vars fished3 vars;
40.1 --- a/src/Tools/Code/code_target.ML Thu Jun 09 15:38:49 2011 +0200
40.2 +++ b/src/Tools/Code/code_target.ML Thu Jun 09 16:34:49 2011 +0200
40.3 @@ -416,7 +416,7 @@
40.4 let
40.5 val _ = if Code_Thingol.contains_dict_var t then
40.6 error "Term to be evaluated contains free dictionaries" else ();
40.7 - val v' = Name.variant (map fst vs) "a";
40.8 + val v' = singleton (Name.variant_list (map fst vs)) "a";
40.9 val vs' = (v', []) :: vs;
40.10 val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty];
40.11 val value_name = "Value.value.value"
41.1 --- a/src/Tools/IsaPlanner/isand.ML Thu Jun 09 15:38:49 2011 +0200
41.2 +++ b/src/Tools/IsaPlanner/isand.ML Thu Jun 09 16:34:49 2011 +0200
41.3 @@ -190,7 +190,7 @@
41.4 val tvars = List.foldr OldTerm.add_term_tvars [] ts;
41.5 val (names',renamings) =
41.6 List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) =>
41.7 - let val n2 = Name.variant Ns n in
41.8 + let val n2 = singleton (Name.variant_list Ns) n in
41.9 (n2::Ns, (tv, (n2,s))::Rs)
41.10 end) (tfree_names @ names,[]) tvars;
41.11 in renamings end;
41.12 @@ -223,7 +223,7 @@
41.13 val Ns = List.foldr OldTerm.add_term_names names ts;
41.14 val (_,renamings) =
41.15 Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) =>
41.16 - let val n2 = Name.variant Ns n in
41.17 + let val n2 = singleton (Name.variant_list Ns) n in
41.18 (n2 :: Ns, (v, (n2,ty)) :: Rs)
41.19 end) ((Ns,[]), vars);
41.20 in renamings end;
42.1 --- a/src/Tools/IsaPlanner/rw_inst.ML Thu Jun 09 15:38:49 2011 +0200
42.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML Thu Jun 09 16:34:49 2011 +0200
42.3 @@ -101,7 +101,7 @@
42.4 val names = usednames_of_thm rule;
42.5 val (fromnames,tonames,names2,Ts') =
42.6 Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) =>
42.7 - let val n2 = Name.variant names n in
42.8 + let val n2 = singleton (Name.variant_list names) n in
42.9 (ctermify (Free(faken,ty)) :: rnf,
42.10 ctermify (Free(n2,ty)) :: rnt,
42.11 n2 :: names,
42.12 @@ -146,7 +146,7 @@
42.13 val vars_to_fix = union (op =) termvars cond_vs;
42.14 val (renamings, names2) =
42.15 List.foldr (fn (((n,i),ty), (vs, names')) =>
42.16 - let val n' = Name.variant names' n in
42.17 + let val n' = singleton (Name.variant_list names') n in
42.18 ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
42.19 end)
42.20 ([], names) vars_to_fix;
42.21 @@ -154,7 +154,7 @@
42.22
42.23 (* make a new fresh typefree instantiation for the given tvar *)
42.24 fun new_tfree (tv as (ix,sort), (pairs,used)) =
42.25 - let val v = Name.variant used (string_of_indexname ix)
42.26 + let val v = singleton (Name.variant_list used) (string_of_indexname ix)
42.27 in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end;
42.28
42.29
43.1 --- a/src/Tools/eqsubst.ML Thu Jun 09 15:38:49 2011 +0200
43.2 +++ b/src/Tools/eqsubst.ML Thu Jun 09 16:34:49 2011 +0200
43.3 @@ -179,7 +179,7 @@
43.4 fun fakefree_badbounds Ts t =
43.5 let val (FakeTs,Ts,newnames) =
43.6 List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) =>
43.7 - let val newname = Name.variant usednames n
43.8 + let val newname = singleton (Name.variant_list usednames) n
43.9 in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
43.10 (newname,ty)::Ts,
43.11 newname::usednames) end)
44.1 --- a/src/ZF/Tools/inductive_package.ML Thu Jun 09 15:38:49 2011 +0200
44.2 +++ b/src/ZF/Tools/inductive_package.ML Thu Jun 09 16:34:49 2011 +0200
44.3 @@ -96,7 +96,7 @@
44.4 Syntax.string_of_term ctxt t);
44.5
44.6 (*** Construct the fixedpoint definition ***)
44.7 - val mk_variant = Name.variant (List.foldr OldTerm.add_term_names [] intr_tms);
44.8 + val mk_variant = singleton (Name.variant_list (List.foldr OldTerm.add_term_names [] intr_tms));
44.9
44.10 val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
44.11
45.1 --- a/src/ZF/Tools/primrec_package.ML Thu Jun 09 15:38:49 2011 +0200
45.2 +++ b/src/ZF/Tools/primrec_package.ML Thu Jun 09 16:34:49 2011 +0200
45.3 @@ -139,8 +139,9 @@
45.4 (** make definition **)
45.5
45.6 (*the recursive argument*)
45.7 - val rec_arg = Free (Name.variant (map #1 (ls@rs)) (Long_Name.base_name big_rec_name),
45.8 - Ind_Syntax.iT)
45.9 + val rec_arg =
45.10 + Free (singleton (Name.variant_list (map #1 (ls@rs))) (Long_Name.base_name big_rec_name),
45.11 + Ind_Syntax.iT)
45.12
45.13 val def_tm = Logic.mk_equals
45.14 (subst_bound (rec_arg, fabs),