--- a/src/HOL/Import/proof_kernel.ML Wed Dec 31 19:56:38 2008 +0100
+++ b/src/HOL/Import/proof_kernel.ML Wed Dec 31 20:31:36 2008 +0100
@@ -1149,8 +1149,8 @@
val t = term_of ct
val thy = theory_of_cterm ct
val frees = OldTerm.term_frees t
- val freenames = OldTerm.add_term_free_names (t, [])
- fun is_old_name n = n mem_string freenames
+ val freenames = Term.add_free_names t []
+ val is_old_name = member (op =) freenames
fun name_of (Free (n, _)) = n
| name_of _ = ERR "name_of"
fun new_name' bump map n =
--- a/src/HOL/Import/shuffler.ML Wed Dec 31 19:56:38 2008 +0100
+++ b/src/HOL/Import/shuffler.ML Wed Dec 31 20:31:36 2008 +0100
@@ -321,7 +321,7 @@
then
let
val cert = cterm_of thy
- val v = Free(Name.variant (OldTerm.add_term_free_names(t,[])) "v",xT)
+ val v = Free (Name.variant (Term.add_free_names t []) "v", xT)
val cv = cert v
val ct = cert t
val th = (assume ct)
@@ -384,7 +384,7 @@
Type("fun",[aT,bT]) =>
let
val cert = cterm_of thy
- val vname = Name.variant (OldTerm.add_term_free_names(t,[])) "v"
+ val vname = Name.variant (Term.add_free_names t []) "v"
val v = Free(vname,aT)
val cv = cert v
val ct = cert t
--- a/src/HOL/Inductive.thy Wed Dec 31 19:56:38 2008 +0100
+++ b/src/HOL/Inductive.thy Wed Dec 31 20:31:36 2008 +0100
@@ -362,7 +362,7 @@
let
fun fun_tr ctxt [cs] =
let
- val x = Free (Name.variant (OldTerm.add_term_free_names (cs, [])) "x", dummyT);
+ val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
val ft = DatatypeCase.case_tr true DatatypePackage.datatype_of_constr
ctxt [x, cs]
in lambda x ft end
--- a/src/HOL/List.thy Wed Dec 31 19:56:38 2008 +0100
+++ b/src/HOL/List.thy Wed Dec 31 20:31:36 2008 +0100
@@ -358,7 +358,7 @@
fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
let
- val x = Free (Name.variant (OldTerm.add_term_free_names (p$e, [])) "x", dummyT);
+ val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
val e = if opti then singl e else e;
val case1 = Syntax.const "_case1" $ p $ e;
val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
--- a/src/HOL/Nominal/nominal_inductive.ML Wed Dec 31 19:56:38 2008 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Wed Dec 31 20:31:36 2008 +0100
@@ -411,7 +411,7 @@
let
val prem :: prems = Logic.strip_imp_prems rule;
val concl = Logic.strip_imp_concl rule;
- val used = OldTerm.add_term_free_names (rule, [])
+ val used = Term.add_free_names rule [];
in
(prem,
List.drop (snd (strip_comb (HOLogic.dest_Trueprop prem)), length ind_params),
--- a/src/HOL/Tools/datatype_case.ML Wed Dec 31 19:56:38 2008 +0100
+++ b/src/HOL/Tools/datatype_case.ML Wed Dec 31 20:31:36 2008 +0100
@@ -54,15 +54,12 @@
* b=false --> i = ~1
*---------------------------------------------------------------------------*)
-fun pattern_map f (tm,x) = (f tm, x);
-
-fun pattern_subst theta = pattern_map (subst_free theta);
+fun pattern_subst theta (tm, x) = (subst_free theta tm, x);
fun row_of_pat x = fst (snd x);
-fun add_row_used ((prfx, pats), (tm, tag)) used =
- foldl OldTerm.add_term_free_names (foldl OldTerm.add_term_free_names
- (OldTerm.add_term_free_names (tm, used)) pats) prfx;
+fun add_row_used ((prfx, pats), (tm, tag)) =
+ fold Term.add_free_names (tm :: pats @ prfx);
(* try to preserve names given by user *)
fun default_names names ts =
@@ -139,7 +136,7 @@
let
val Ts = map type_of rstp;
val xs = Name.variant_list
- (foldl OldTerm.add_term_free_names used' gvars)
+ (fold Term.add_free_names gvars used')
(replicate (length rstp) "x")
in
[((prfx, gvars @ map Free (xs ~~ Ts)),
@@ -221,7 +218,7 @@
| SOME {case_name, constructors} =>
let
val pty = body_type cT;
- val used' = foldl OldTerm.add_term_free_names used rstp;
+ val used' = fold Term.add_free_names rstp used;
val nrows = maps (expand constructors used' pty) rows;
val subproblems = partition ty_match ty_inst type_of used'
constructors pty range_ty nrows;
@@ -335,7 +332,7 @@
| prep_pat t used = case_error ("Bad pattern: " ^ Syntax.string_of_term ctxt t);
fun dest_case1 (t as Const ("_case1", _) $ l $ r) =
let val (l', cnstrts) = strip_constraints l
- in ((fst (prep_pat l' (OldTerm.add_term_free_names (t, []))), r), cnstrts)
+ in ((fst (prep_pat l' (Term.add_free_names t [])), r), cnstrts)
end
| dest_case1 t = case_error "dest_case1";
fun dest_case2 (Const ("_case2", _) $ t $ u) = t :: dest_case2 u
@@ -423,7 +420,7 @@
(* destruct nested patterns *)
fun strip_case' dest (pat, rhs) =
- case dest (OldTerm.add_term_free_names (pat, [])) rhs of
+ case dest (Term.add_free_names pat []) rhs of
SOME (exp as Free _, clauses) =>
if member op aconv (OldTerm.term_frees pat) exp andalso
not (exists (fn (_, rhs') =>
--- a/src/HOL/Tools/inductive_realizer.ML Wed Dec 31 19:56:38 2008 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Dec 31 20:31:36 2008 +0100
@@ -49,7 +49,7 @@
t $ strip_all' used names Q
| strip_all' _ _ t = t;
-fun strip_all t = strip_all' (OldTerm.add_term_free_names (t, [])) [] t;
+fun strip_all t = strip_all' (Term.add_free_names t []) [] t;
fun strip_one name (Const ("all", _) $ Abs (s, T, Const ("==>", _) $ P $ Q)) =
(subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
@@ -370,7 +370,7 @@
(vs' @ Ps) rec_names rss' intrs dummies;
val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs' @ Ps) r
(prop_of ind)) (rs ~~ inducts);
- val used = foldr OldTerm.add_term_free_names [] rlzs;
+ val used = fold Term.add_free_names rlzs [];
val rnames = Name.variant_list used (replicate (length inducts) "r");
val rnames' = Name.variant_list
(used @ rnames) (replicate (length intrs) "s");