# HG changeset patch # User wenzelm # Date 1230751896 -3600 # Node ID b22ccb3998db5ca09809d1f5a3bfe8df418ae1df # Parent c5531bf7c6b2c33eaa2efdbd910027e907db4274 eliminated OldTerm.add_term_free_names; diff -r c5531bf7c6b2 -r b22ccb3998db src/HOL/Import/proof_kernel.ML --- 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 = diff -r c5531bf7c6b2 -r b22ccb3998db src/HOL/Import/shuffler.ML --- 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 diff -r c5531bf7c6b2 -r b22ccb3998db src/HOL/Inductive.thy --- 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 diff -r c5531bf7c6b2 -r b22ccb3998db src/HOL/List.thy --- 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 diff -r c5531bf7c6b2 -r b22ccb3998db src/HOL/Nominal/nominal_inductive.ML --- 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), diff -r c5531bf7c6b2 -r b22ccb3998db src/HOL/Tools/datatype_case.ML --- 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') => diff -r c5531bf7c6b2 -r b22ccb3998db src/HOL/Tools/inductive_realizer.ML --- 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");