# HG changeset patch
# User wenzelm
# Date 1230816219 -3600
# Node ID 5b0bfd63b5da3f8e01d03ebc0d0ea0ad1bb707c3
# Parent  5de880bda02d3359f7e8bc19e5dc4a514d071a0d
eliminated OldTerm.(add_)term_consts;

diff -r 5de880bda02d -r 5b0bfd63b5da src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Thu Jan 01 14:23:38 2009 +0100
+++ b/src/HOL/Import/shuffler.ML	Thu Jan 01 14:23:39 2009 +0100
@@ -572,8 +572,8 @@
     fold_rev (fn thm => fn cs =>
               let
                   val (lhs,rhs) = Logic.dest_equals (prop_of thm)
-                  val ignore_lhs = OldTerm.term_consts lhs \\ OldTerm.term_consts rhs
-                  val ignore_rhs = OldTerm.term_consts rhs \\ OldTerm.term_consts lhs
+                  val ignore_lhs = Term.add_const_names lhs [] \\ Term.add_const_names rhs []
+                  val ignore_rhs = Term.add_const_names rhs [] \\ Term.add_const_names lhs []
               in
                   fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs)
               end)
diff -r 5de880bda02d -r 5b0bfd63b5da src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Thu Jan 01 14:23:38 2009 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Thu Jan 01 14:23:39 2009 +0100
@@ -169,7 +169,7 @@
 fun eqn_suc_preproc thy ths =
   let
     val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of;
-    fun contains_suc t = member (op =) (OldTerm.term_consts t) @{const_name Suc};
+    val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
   in
     if forall (can dest) ths andalso
       exists (contains_suc o dest) ths
@@ -211,8 +211,8 @@
     val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
   in
     if forall (can (dest o concl_of)) ths andalso
-      exists (fn th => member (op =) (foldr OldTerm.add_term_consts
-        [] (map_filter (try dest) (concl_of th :: prems_of th))) "Suc") ths
+      exists (fn th => exists (exists_Const (fn (c, _) => c = @{const_name Suc}))
+        (map_filter (try dest) (concl_of th :: prems_of th))) ths
     then remove_suc_clause thy ths else ths
   end;
 
diff -r 5de880bda02d -r 5b0bfd63b5da src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Thu Jan 01 14:23:38 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Jan 01 14:23:39 2009 +0100
@@ -152,7 +152,7 @@
     val elims = map (atomize_induct ctxt) elims;
     val monos = InductivePackage.get_monos ctxt;
     val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
-    val _ = (case names \\ foldl (apfst prop_of #> OldTerm.add_term_consts) [] eqvt_thms of
+    val _ = (case names \\ fold (Term.add_const_names o Thm.prop_of) eqvt_thms [] of
         [] => ()
       | xs => error ("Missing equivariance theorem for predicate(s): " ^
           commas_quote xs));
diff -r 5de880bda02d -r 5b0bfd63b5da src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Jan 01 14:23:38 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Thu Jan 01 14:23:39 2009 +0100
@@ -158,7 +158,7 @@
     val elims = map (atomize_induct ctxt) elims;
     val monos = InductivePackage.get_monos ctxt;
     val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
-    val _ = (case names \\ foldl (apfst prop_of #> OldTerm.add_term_consts) [] eqvt_thms of
+    val _ = (case names \\ fold (Term.add_const_names o Thm.prop_of) eqvt_thms [] of
         [] => ()
       | xs => error ("Missing equivariance theorem for predicate(s): " ^
           commas_quote xs));
diff -r 5de880bda02d -r 5b0bfd63b5da src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Thu Jan 01 14:23:38 2009 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Thu Jan 01 14:23:39 2009 +0100
@@ -57,7 +57,7 @@
       | _ => (warn thm; thy))
     | SOME (Const (s, _), _) =>
         let
-          val cs = foldr OldTerm.add_term_consts [] (prems_of thm);
+          val cs = fold Term.add_const_names (Thm.prems_of thm) [];
           val rules = Symtab.lookup_list intros s;
           val nparms = (case optnparms of
             SOME k => k
@@ -490,7 +490,7 @@
       | SOME (names, thyname, nparms, intrs) =>
           mk_ind_def thy defs gr dep names (if_library thyname module)
             [] (prep_intrs intrs) nparms))
-            (gr, foldr OldTerm.add_term_consts [] ts)
+            (gr, fold Term.add_const_names ts [])
 
 and mk_ind_def thy defs gr dep names module modecs intrs nparms =
   add_edge_acyclic (hd names, dep) gr handle
diff -r 5de880bda02d -r 5b0bfd63b5da src/Pure/old_term.ML
--- a/src/Pure/old_term.ML	Thu Jan 01 14:23:38 2009 +0100
+++ b/src/Pure/old_term.ML	Thu Jan 01 14:23:39 2009 +0100
@@ -14,7 +14,6 @@
   val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
   val add_term_tfrees: term * (string * sort) list -> (string * sort) list
   val add_term_tfree_names: term * string list -> string list
-  val add_term_consts: term * string list -> string list
   val typ_tfrees: typ -> (string * sort) list
   val typ_tvars: typ -> (indexname * sort) list
   val term_tfrees: term -> (string * sort) list
@@ -23,7 +22,6 @@
   val term_vars: term -> term list
   val add_term_frees: term * term list -> term list
   val term_frees: term -> term list
-  val term_consts: term -> string list
 end;
 
 structure OldTerm: OLD_TERM =
@@ -68,17 +66,11 @@
 val add_term_tfrees = it_term_types add_typ_tfrees;
 val add_term_tfree_names = it_term_types add_typ_tfree_names;
 
-fun add_term_consts (Const (c, _), cs) = insert (op =) c cs
-  | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
-  | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
-  | add_term_consts (_, cs) = cs;
-
 (*Non-list versions*)
 fun typ_tfrees T = add_typ_tfrees(T,[]);
 fun typ_tvars T = add_typ_tvars(T,[]);
 fun term_tfrees t = add_term_tfrees(t,[]);
 fun term_tvars t = add_term_tvars(t,[]);
-fun term_consts t = add_term_consts(t,[]);
 
 
 (*Accumulates the Vars in the term, suppressing duplicates.*)