eliminated OldTerm.add_term_free_names;
authorwenzelm
Wed Dec 31 20:31:36 2008 +0100 (2008-12-31)
changeset 29281b22ccb3998db
parent 29280 c5531bf7c6b2
child 29282 40a1014cefaa
eliminated OldTerm.add_term_free_names;
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Inductive.thy
src/HOL/List.thy
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Tools/datatype_case.ML
src/HOL/Tools/inductive_realizer.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Dec 31 19:56:38 2008 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Dec 31 20:31:36 2008 +0100
     1.3 @@ -1149,8 +1149,8 @@
     1.4        val t = term_of ct
     1.5        val thy = theory_of_cterm ct
     1.6        val frees = OldTerm.term_frees t
     1.7 -      val freenames = OldTerm.add_term_free_names (t, [])
     1.8 -      fun is_old_name n = n mem_string freenames
     1.9 +      val freenames = Term.add_free_names t []
    1.10 +      val is_old_name = member (op =) freenames
    1.11        fun name_of (Free (n, _)) = n
    1.12          | name_of _ = ERR "name_of"
    1.13        fun new_name' bump map n =
     2.1 --- a/src/HOL/Import/shuffler.ML	Wed Dec 31 19:56:38 2008 +0100
     2.2 +++ b/src/HOL/Import/shuffler.ML	Wed Dec 31 20:31:36 2008 +0100
     2.3 @@ -321,7 +321,7 @@
     2.4                then
     2.5                    let
     2.6                        val cert = cterm_of thy
     2.7 -                      val v = Free(Name.variant (OldTerm.add_term_free_names(t,[])) "v",xT)
     2.8 +                      val v = Free (Name.variant (Term.add_free_names t []) "v", xT)
     2.9                        val cv = cert v
    2.10                        val ct = cert t
    2.11                        val th = (assume ct)
    2.12 @@ -384,7 +384,7 @@
    2.13                        Type("fun",[aT,bT]) =>
    2.14                        let
    2.15                            val cert = cterm_of thy
    2.16 -                          val vname = Name.variant (OldTerm.add_term_free_names(t,[])) "v"
    2.17 +                          val vname = Name.variant (Term.add_free_names t []) "v"
    2.18                            val v = Free(vname,aT)
    2.19                            val cv = cert v
    2.20                            val ct = cert t
     3.1 --- a/src/HOL/Inductive.thy	Wed Dec 31 19:56:38 2008 +0100
     3.2 +++ b/src/HOL/Inductive.thy	Wed Dec 31 20:31:36 2008 +0100
     3.3 @@ -362,7 +362,7 @@
     3.4  let
     3.5    fun fun_tr ctxt [cs] =
     3.6      let
     3.7 -      val x = Free (Name.variant (OldTerm.add_term_free_names (cs, [])) "x", dummyT);
     3.8 +      val x = Free (Name.variant (Term.add_free_names cs []) "x", dummyT);
     3.9        val ft = DatatypeCase.case_tr true DatatypePackage.datatype_of_constr
    3.10                   ctxt [x, cs]
    3.11      in lambda x ft end
     4.1 --- a/src/HOL/List.thy	Wed Dec 31 19:56:38 2008 +0100
     4.2 +++ b/src/HOL/List.thy	Wed Dec 31 20:31:36 2008 +0100
     4.3 @@ -358,7 +358,7 @@
     4.4  
     4.5     fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
     4.6      let
     4.7 -      val x = Free (Name.variant (OldTerm.add_term_free_names (p$e, [])) "x", dummyT);
     4.8 +      val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
     4.9        val e = if opti then singl e else e;
    4.10        val case1 = Syntax.const "_case1" $ p $ e;
    4.11        val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
     5.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Dec 31 19:56:38 2008 +0100
     5.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Dec 31 20:31:36 2008 +0100
     5.3 @@ -411,7 +411,7 @@
     5.4        let
     5.5          val prem :: prems = Logic.strip_imp_prems rule;
     5.6          val concl = Logic.strip_imp_concl rule;
     5.7 -        val used = OldTerm.add_term_free_names (rule, [])
     5.8 +        val used = Term.add_free_names rule [];
     5.9        in
    5.10          (prem,
    5.11           List.drop (snd (strip_comb (HOLogic.dest_Trueprop prem)), length ind_params),
     6.1 --- a/src/HOL/Tools/datatype_case.ML	Wed Dec 31 19:56:38 2008 +0100
     6.2 +++ b/src/HOL/Tools/datatype_case.ML	Wed Dec 31 20:31:36 2008 +0100
     6.3 @@ -54,15 +54,12 @@
     6.4   * b=false --> i = ~1
     6.5   *---------------------------------------------------------------------------*)
     6.6  
     6.7 -fun pattern_map f (tm,x) = (f tm, x);
     6.8 -
     6.9 -fun pattern_subst theta = pattern_map (subst_free theta);
    6.10 +fun pattern_subst theta (tm, x) = (subst_free theta tm, x);
    6.11  
    6.12  fun row_of_pat x = fst (snd x);
    6.13  
    6.14 -fun add_row_used ((prfx, pats), (tm, tag)) used =
    6.15 -  foldl OldTerm.add_term_free_names (foldl OldTerm.add_term_free_names
    6.16 -    (OldTerm.add_term_free_names (tm, used)) pats) prfx;
    6.17 +fun add_row_used ((prfx, pats), (tm, tag)) =
    6.18 +  fold Term.add_free_names (tm :: pats @ prfx);
    6.19  
    6.20  (* try to preserve names given by user *)
    6.21  fun default_names names ts =
    6.22 @@ -139,7 +136,7 @@
    6.23                      let
    6.24                        val Ts = map type_of rstp;
    6.25                        val xs = Name.variant_list
    6.26 -                        (foldl OldTerm.add_term_free_names used' gvars)
    6.27 +                        (fold Term.add_free_names gvars used')
    6.28                          (replicate (length rstp) "x")
    6.29                      in
    6.30                        [((prfx, gvars @ map Free (xs ~~ Ts)),
    6.31 @@ -221,7 +218,7 @@
    6.32                | SOME {case_name, constructors} =>
    6.33                  let
    6.34                    val pty = body_type cT;
    6.35 -                  val used' = foldl OldTerm.add_term_free_names used rstp;
    6.36 +                  val used' = fold Term.add_free_names rstp used;
    6.37                    val nrows = maps (expand constructors used' pty) rows;
    6.38                    val subproblems = partition ty_match ty_inst type_of used'
    6.39                      constructors pty range_ty nrows;
    6.40 @@ -335,7 +332,7 @@
    6.41          | prep_pat t used = case_error ("Bad pattern: " ^ Syntax.string_of_term ctxt t);
    6.42        fun dest_case1 (t as Const ("_case1", _) $ l $ r) =
    6.43              let val (l', cnstrts) = strip_constraints l
    6.44 -            in ((fst (prep_pat l' (OldTerm.add_term_free_names (t, []))), r), cnstrts)
    6.45 +            in ((fst (prep_pat l' (Term.add_free_names t [])), r), cnstrts)
    6.46              end
    6.47          | dest_case1 t = case_error "dest_case1";
    6.48        fun dest_case2 (Const ("_case2", _) $ t $ u) = t :: dest_case2 u
    6.49 @@ -423,7 +420,7 @@
    6.50  (* destruct nested patterns *)
    6.51  
    6.52  fun strip_case' dest (pat, rhs) =
    6.53 -  case dest (OldTerm.add_term_free_names (pat, [])) rhs of
    6.54 +  case dest (Term.add_free_names pat []) rhs of
    6.55      SOME (exp as Free _, clauses) =>
    6.56        if member op aconv (OldTerm.term_frees pat) exp andalso
    6.57          not (exists (fn (_, rhs') =>
     7.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Dec 31 19:56:38 2008 +0100
     7.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Dec 31 20:31:36 2008 +0100
     7.3 @@ -49,7 +49,7 @@
     7.4        t $ strip_all' used names Q
     7.5    | strip_all' _ _ t = t;
     7.6  
     7.7 -fun strip_all t = strip_all' (OldTerm.add_term_free_names (t, [])) [] t;
     7.8 +fun strip_all t = strip_all' (Term.add_free_names t []) [] t;
     7.9  
    7.10  fun strip_one name (Const ("all", _) $ Abs (s, T, Const ("==>", _) $ P $ Q)) =
    7.11        (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
    7.12 @@ -370,7 +370,7 @@
    7.13            (vs' @ Ps) rec_names rss' intrs dummies;
    7.14          val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs' @ Ps) r
    7.15            (prop_of ind)) (rs ~~ inducts);
    7.16 -        val used = foldr OldTerm.add_term_free_names [] rlzs;
    7.17 +        val used = fold Term.add_free_names rlzs [];
    7.18          val rnames = Name.variant_list used (replicate (length inducts) "r");
    7.19          val rnames' = Name.variant_list
    7.20            (used @ rnames) (replicate (length intrs) "s");