2008-12-31 wenzelm [Wed, 31 Dec 2008 18:53:19 +0100] rev 29275
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
use regular Term.add_XXX etc.;
src/Pure/Isar/locale.ML src/Pure/type.ML src/Tools/Compute_Oracle/linker.ML

2008-12-31 wenzelm [Wed, 31 Dec 2008 18:53:18 +0100] rev 29274
use fold_aterms directly;
src/Pure/Isar/find_theorems.ML

2008-12-31 wenzelm [Wed, 31 Dec 2008 18:53:18 +0100] rev 29273
use exists_Const directly;
src/HOL/ex/reflection.ML src/Provers/coherent.ML

2008-12-31 wenzelm [Wed, 31 Dec 2008 18:53:17 +0100] rev 29272
use regular Term.add_XXX etc.;
src/HOL/Tools/recfun_codegen.ML src/HOL/Tools/refute.ML src/HOL/Tools/res_reconstruct.ML src/HOL/Tools/typecopy_package.ML src/Pure/Isar/expression.ML src/Pure/tctical.ML src/Pure/thm.ML src/Tools/code/code_thingol.ML src/Tools/nbe.ML

2008-12-31 wenzelm [Wed, 31 Dec 2008 18:53:16 +0100] rev 29271
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
use exists_Const directly;
src/HOL/Tools/inductive_realizer.ML src/Pure/Proof/proof_rewrite_rules.ML

2008-12-31 wenzelm [Wed, 31 Dec 2008 18:53:16 +0100] rev 29270
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
src/HOL/Import/proof_kernel.ML src/HOL/Import/shuffler.ML src/HOL/Inductive.thy src/HOL/Library/Efficient_Nat.thy src/HOL/List.thy src/HOL/Matrix/cplex/matrixlp.ML src/HOL/Modelcheck/mucke_oracle.ML src/HOL/Nominal/nominal_inductive.ML src/HOL/Nominal/nominal_inductive2.ML src/HOL/Nominal/nominal_package.ML src/HOL/Tools/TFL/casesplit.ML src/HOL/Tools/TFL/rules.ML src/HOL/Tools/TFL/tfl.ML src/HOL/Tools/TFL/usyntax.ML src/HOL/Tools/datatype_abs_proofs.ML src/HOL/Tools/datatype_case.ML src/HOL/Tools/datatype_codegen.ML src/HOL/Tools/datatype_package.ML src/HOL/Tools/datatype_prop.ML src/HOL/Tools/datatype_rep_proofs.ML src/HOL/Tools/inductive_codegen.ML src/HOL/Tools/record_package.ML src/HOL/Tools/res_atp.ML src/HOL/Tools/res_axioms.ML src/Pure/Isar/code_unit.ML src/Pure/Proof/extraction.ML src/Pure/Proof/proofchecker.ML src/Pure/Proof/reconstruct.ML src/Pure/codegen.ML src/Pure/drule.ML src/Pure/old_term.ML src/Pure/proofterm.ML src/Pure/term.ML src/Tools/IsaPlanner/isand.ML src/Tools/IsaPlanner/rw_inst.ML src/ZF/Tools/inductive_package.ML

2008-12-31 wenzelm [Wed, 31 Dec 2008 15:30:10 +0100] rev 29269
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;
src/CCL/Wfd.thy src/FOLP/IFOLP.thy src/HOL/Algebra/abstract/Ring2.thy src/HOL/Algebra/ringsimp.ML src/HOL/Import/shuffler.ML src/HOL/OrderedGroup.thy src/HOL/Statespace/DistinctTreeProver.thy src/HOL/Statespace/distinct_tree_prover.ML src/HOL/Tools/Groebner_Basis/groebner.ML src/HOL/Tools/Groebner_Basis/normalizer.ML src/HOL/Tools/Qelim/langford.ML src/HOL/Tools/Qelim/presburger.ML src/HOL/Tools/function_package/decompose.ML src/HOL/Tools/function_package/termination.ML src/HOL/Tools/int_arith.ML src/HOL/Tools/nat_simprocs.ML src/HOL/Tools/sat_funcs.ML src/HOL/ex/reflection.ML src/Provers/Arith/cancel_factor.ML src/Provers/Arith/cancel_sums.ML src/Provers/eqsubst.ML src/Pure/IsaMakefile src/Pure/Isar/find_theorems.ML src/Pure/Isar/locale.ML src/Pure/Isar/rule_cases.ML src/Pure/ROOT.ML src/Pure/envir.ML src/Pure/facts.ML src/Pure/meta_simplifier.ML src/Pure/more_thm.ML src/Pure/old_term.ML src/Pure/pattern.ML src/Pure/proofterm.ML src/Pure/search.ML src/Pure/sorts.ML src/Pure/term.ML src/Pure/term_ord.ML src/Pure/term_subst.ML src/Pure/thm.ML src/Pure/type.ML src/Pure/unify.ML src/Sequents/modal.ML src/Sequents/prover.ML src/Tools/Compute_Oracle/compute.ML src/Tools/Compute_Oracle/linker.ML src/ZF/arith_data.ML src/ZF/int_arith.ML

2008-12-31 wenzelm [Wed, 31 Dec 2008 00:08:14 +0100] rev 29268
use exists_subterm directly;
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
src/HOL/Tools/res_reconstruct.ML

2008-12-31 wenzelm [Wed, 31 Dec 2008 00:08:13 +0100] rev 29267
use exists_subterm directly;
src/HOL/Tools/meson.ML src/HOL/Tools/res_atp.ML src/Provers/classical.ML

2008-12-31 wenzelm [Wed, 31 Dec 2008 00:08:13 +0100] rev 29266
use regular Term.add_vars, Term.add_frees etc.;
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
src/HOL/Tools/datatype_case.ML src/HOL/Tools/metis_tools.ML src/HOL/Tools/old_primrec_package.ML src/Pure/codegen.ML src/Tools/quickcheck.ML src/ZF/Tools/primrec_package.ML