proof_body/pthm: removed redundant types field;

fold_proof_atoms: unified recursive case with fold_body_thms;

tuned signature;

fold_proof_atoms: unified recursive case with fold_body_thms;

tuned signature;

clarified Thm.proof_body_of vs. Thm.proof_of;

src/HOL/Tools/datatype_realizer.ML src/HOL/Tools/inductive_realizer.ML src/HOL/Tools/rewrite_hol_proof.ML src/Pure/Isar/isar_cmd.ML src/Pure/Proof/extraction.ML src/Pure/Proof/proof_syntax.ML src/Pure/ProofGeneral/proof_general_pgip.ML src/Pure/Thy/thm_deps.ML src/Pure/thm.ML

- Corrected order of quantification over Frees.

- Fixed bug in handling of TFrees that caused variable order to get mixed up.

- Fixed bug in handling of TFrees that caused variable order to get mixed up.

Frees in PThms are now quantified in the order of their appearance in the

proposition as well, to make it compatible (again) with variable order used

by forall_intr_frees.

proposition as well, to make it compatible (again) with variable order used

by forall_intr_frees.

retrieve thm deps from proof_body;

removed obsolete enable/disable operation;

removed obsolete enable/disable operation;

proof_of_term: removed obsolete disambiguisation table;

adapted PThm;

Thm.proof_of returns proof_body;

adapted PThm;

Thm.proof_of returns proof_body;