src/Pure/theory_data.ML

- Moved rewriting functions to meta_simplifier.ML
- dest_abs now also takes an optional variable name as an argument
- beta_conversion takes additional flag as an argument. Fully reduces
the term if set to true

Some tuning:
- tuned fix_shyps in instantiate, implies_intr, implies_elim, reflexive,
transitive, beta_conversion, abstract_rule
- combination: chktypes derives types of f and t from type of == instead
of using fastype_of

New primitives:
- eta_conversion
- incr_indexes: increment indexes in theorems
- cterm_incr_indexes: increment indexes in cterms
- cterm_match, cterm_first_order_match
- rename_boundvars

(*  Title:      Pure/theory_data.ML
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Type-safe interface for theory data.
*)

signature THEORY_DATA_ARGS =
sig
  val name: string
  type T
  val empty: T
  val copy: T -> T
  val prep_ext: T -> T
  val merge: T * T -> T
  val print: Sign.sg -> T -> unit
end;

signature THEORY_DATA =
sig
  type T
  val init: theory -> theory
  val print: theory -> unit
  val get_sg: Sign.sg -> T
  val get: theory -> T
  val put: T -> theory -> theory
  val map: (T -> T) -> theory -> theory
end;

functor TheoryDataFun(Args: THEORY_DATA_ARGS): THEORY_DATA =
struct

(*object kind kept private!*)
val kind = Object.kind Args.name;

type T = Args.T;
exception Data of T;

val init =
  Theory.init_data kind
    (Data Args.empty,
      fn (Data x) => Data (Args.copy x),
      fn (Data x) => Data (Args.prep_ext x),
      fn (Data x1, Data x2) => Data (Args.merge (x1, x2)),
      fn sg => fn (Data x) => Args.print sg x);

val print = Theory.print_data kind;
val get_sg = Sign.get_data kind (fn Data x => x);
val get = get_sg o Theory.sign_of;
val put = Theory.put_data kind Data;
fun map f thy = put (f (get thy)) thy;

end;

(*hide private data access functions*)
structure Sign: SIGN = Sign;
structure Theory: THEORY = Theory;