more tight filtering;

tuned;

tuned -- maxidx unused;

tuned;

clarified name of Type.unified, to emphasize its connection to the "unify" family;
tuned low-level operation;

tuned;

tuned signature;

tuned;

tuned signature;

tuned signature -- slightly more general operations (cf. term.ML);

tuned signature;

make SML/NJ happy;

tuned exceptions -- avoid composing error messages in low-level situations;

tuned signature;
tuned comments;

more robust exception pattern General.Subscript;

added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;

modernized structure Term_Ord;

eliminated dead code;

Correct chasing of type variable instantiations during type unification.
The following theory should not raise exception TERM:

constdefs
somepredicate :: "(('b => 'b) => ('a => 'a))
=> 'a => 'b => bool"
"somepredicate upd v x == True"

lemma somepredicate_idI:
"somepredicate id (f v) v"
by (simp add: somepredicate_def)

lemma somepredicate_triv:
"somepredicate upd v x ==> somepredicate upd v x"
by assumption

lemmas somepredicate_triv [OF somepredicate_idI]

lemmas st' = somepredicate_triv[where v="h :: nat => bool"]

lemmas st2 = st'[OF somepredicate_idI]

tuned/modernized subst: Same.operation;
renamed typ_subst_TVars to subst_type;
renamed subst_TVars to subst_term_types;
renamed subst_vars to subst_term;
removed unused subst_Vars (covered by subst_term);

major cleanup, simplification, modernization;

use structure Same;
tuned signature;
tuned comments;
tuned;

Merge.

eliminated NJ's List.nth;

moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;

added insert_sorts (from thm.ML);

Type.lookup now curried

Optimized beta_norm: only tries to normalize term when it contains
abstractions.

Term.has_abs;

Term.string_of_vname;

tuned eta_contract;

added expand_term_frees;

added expand_term;

tuned eta_contract;

renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);

removed obsolete xless;

tuned Seq/Envir/Unify interfaces;

expand_atom: Type.raw_match;

added (beta_)eta_contract (from pattern.ML);
added expand_atom;

TableFun/Symtab: curried lookup and update;

curried_lookup/update;

Fixed bug: lookup' must use = instead of eq_type to compare types of
variables, otherwise pattern matching algorithm may loop.

- Eliminated nodup_vars check.
- Unification and matching functions now check types of term variables / sorts
of type variables when applying a substitution.
- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list
as argument, to allow for proper instantiation of theorems containing
type variables with same name but different sorts.

Move towards standard functions.

Deleted Library.option type.

added type_env function;
let norm_type_XXX work directly with type env component;

Moved head_norm and fastype from unify.ML to envir.ML

- exported SAME exception
- exported functions for normalizing types

added beta_norm;
tuned;

Envir now uses Vartab instead of association lists.

fixed comment;

Speedups involving norm

In-lined the one function call to normTsh

Deleted Olist constructor. Replaced minidx by "above" function

Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.

inserted tabs again

removed tabs

Pure/envir/norm_term: replaced equality test for [] by null

added is_empty: env -> bool, minidx: env -> int option;

Initial revision