eliminated OldTerm.(add_)term_consts;
authorwenzelm
Thu Jan 01 14:23:39 2009 +0100 (2009-01-01)
changeset 292875b0bfd63b5da
parent 29286 5de880bda02d
child 29288 253bcf2a5854
eliminated OldTerm.(add_)term_consts;
src/HOL/Import/shuffler.ML
src/HOL/Library/Efficient_Nat.thy
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Tools/inductive_codegen.ML
src/Pure/old_term.ML
     1.1 --- a/src/HOL/Import/shuffler.ML	Thu Jan 01 14:23:38 2009 +0100
     1.2 +++ b/src/HOL/Import/shuffler.ML	Thu Jan 01 14:23:39 2009 +0100
     1.3 @@ -572,8 +572,8 @@
     1.4      fold_rev (fn thm => fn cs =>
     1.5                let
     1.6                    val (lhs,rhs) = Logic.dest_equals (prop_of thm)
     1.7 -                  val ignore_lhs = OldTerm.term_consts lhs \\ OldTerm.term_consts rhs
     1.8 -                  val ignore_rhs = OldTerm.term_consts rhs \\ OldTerm.term_consts lhs
     1.9 +                  val ignore_lhs = Term.add_const_names lhs [] \\ Term.add_const_names rhs []
    1.10 +                  val ignore_rhs = Term.add_const_names rhs [] \\ Term.add_const_names lhs []
    1.11                in
    1.12                    fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs)
    1.13                end)
     2.1 --- a/src/HOL/Library/Efficient_Nat.thy	Thu Jan 01 14:23:38 2009 +0100
     2.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Jan 01 14:23:39 2009 +0100
     2.3 @@ -169,7 +169,7 @@
     2.4  fun eqn_suc_preproc thy ths =
     2.5    let
     2.6      val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of;
     2.7 -    fun contains_suc t = member (op =) (OldTerm.term_consts t) @{const_name Suc};
     2.8 +    val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
     2.9    in
    2.10      if forall (can dest) ths andalso
    2.11        exists (contains_suc o dest) ths
    2.12 @@ -211,8 +211,8 @@
    2.13      val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
    2.14    in
    2.15      if forall (can (dest o concl_of)) ths andalso
    2.16 -      exists (fn th => member (op =) (foldr OldTerm.add_term_consts
    2.17 -        [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths
    2.18 +      exists (fn th => exists (exists_Const (fn (c, _) => c = @{const_name Suc}))
    2.19 +        (map_filter (try dest) (concl_of th :: prems_of th))) ths
    2.20      then remove_suc_clause thy ths else ths
    2.21    end;
    2.22  
     3.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Jan 01 14:23:38 2009 +0100
     3.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Jan 01 14:23:39 2009 +0100
     3.3 @@ -152,7 +152,7 @@
     3.4      val elims = map (atomize_induct ctxt) elims;
     3.5      val monos = InductivePackage.get_monos ctxt;
     3.6      val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
     3.7 -    val _ = (case names \\ foldl (apfst prop_of #> OldTerm.add_term_consts) [] eqvt_thms of
     3.8 +    val _ = (case names \\ fold (Term.add_const_names o Thm.prop_of) eqvt_thms [] of
     3.9          [] => ()
    3.10        | xs => error ("Missing equivariance theorem for predicate(s): " ^
    3.11            commas_quote xs));
     4.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Jan 01 14:23:38 2009 +0100
     4.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Thu Jan 01 14:23:39 2009 +0100
     4.3 @@ -158,7 +158,7 @@
     4.4      val elims = map (atomize_induct ctxt) elims;
     4.5      val monos = InductivePackage.get_monos ctxt;
     4.6      val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
     4.7 -    val _ = (case names \\ foldl (apfst prop_of #> OldTerm.add_term_consts) [] eqvt_thms of
     4.8 +    val _ = (case names \\ fold (Term.add_const_names o Thm.prop_of) eqvt_thms [] of
     4.9          [] => ()
    4.10        | xs => error ("Missing equivariance theorem for predicate(s): " ^
    4.11            commas_quote xs));
     5.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Jan 01 14:23:38 2009 +0100
     5.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Jan 01 14:23:39 2009 +0100
     5.3 @@ -57,7 +57,7 @@
     5.4        | _ => (warn thm; thy))
     5.5      | SOME (Const (s, _), _) =>
     5.6          let
     5.7 -          val cs = foldr OldTerm.add_term_consts [] (prems_of thm);
     5.8 +          val cs = fold Term.add_const_names (Thm.prems_of thm) [];
     5.9            val rules = Symtab.lookup_list intros s;
    5.10            val nparms = (case optnparms of
    5.11              SOME k => k
    5.12 @@ -490,7 +490,7 @@
    5.13        | SOME (names, thyname, nparms, intrs) =>
    5.14            mk_ind_def thy defs gr dep names (if_library thyname module)
    5.15              [] (prep_intrs intrs) nparms))
    5.16 -            (gr, foldr OldTerm.add_term_consts [] ts)
    5.17 +            (gr, fold Term.add_const_names ts [])
    5.18  
    5.19  and mk_ind_def thy defs gr dep names module modecs intrs nparms =
    5.20    add_edge_acyclic (hd names, dep) gr handle
     6.1 --- a/src/Pure/old_term.ML	Thu Jan 01 14:23:38 2009 +0100
     6.2 +++ b/src/Pure/old_term.ML	Thu Jan 01 14:23:39 2009 +0100
     6.3 @@ -14,7 +14,6 @@
     6.4    val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
     6.5    val add_term_tfrees: term * (string * sort) list -> (string * sort) list
     6.6    val add_term_tfree_names: term * string list -> string list
     6.7 -  val add_term_consts: term * string list -> string list
     6.8    val typ_tfrees: typ -> (string * sort) list
     6.9    val typ_tvars: typ -> (indexname * sort) list
    6.10    val term_tfrees: term -> (string * sort) list
    6.11 @@ -23,7 +22,6 @@
    6.12    val term_vars: term -> term list
    6.13    val add_term_frees: term * term list -> term list
    6.14    val term_frees: term -> term list
    6.15 -  val term_consts: term -> string list
    6.16  end;
    6.17  
    6.18  structure OldTerm: OLD_TERM =
    6.19 @@ -68,17 +66,11 @@
    6.20  val add_term_tfrees = it_term_types add_typ_tfrees;
    6.21  val add_term_tfree_names = it_term_types add_typ_tfree_names;
    6.22  
    6.23 -fun add_term_consts (Const (c, _), cs) = insert (op =) c cs
    6.24 -  | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
    6.25 -  | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
    6.26 -  | add_term_consts (_, cs) = cs;
    6.27 -
    6.28  (*Non-list versions*)
    6.29  fun typ_tfrees T = add_typ_tfrees(T,[]);
    6.30  fun typ_tvars T = add_typ_tvars(T,[]);
    6.31  fun term_tfrees t = add_term_tfrees(t,[]);
    6.32  fun term_tvars t = add_term_tvars(t,[]);
    6.33 -fun term_consts t = add_term_consts(t,[]);
    6.34  
    6.35  
    6.36  (*Accumulates the Vars in the term, suppressing duplicates.*)