tuned header;

Thomas Sewell, NICTA: more efficient HOL/record implementation;

tuned whitespace -- recover basic Isabelle conventions;

merged

Merge with isabelle dev changes.

Replace OldTerm.term_vars with Term.add_vars in named_cterm_instantiate.

Avoid a possible variable name conflict in instantiating a theorem. Instantiating a theorem variable with new variables created a possible variable name conflict if a record was defined with a field named 'f', 'x' etc. Using variable indices of 1 avoids the problem.

Fix unescaped expressions breaking latex output in Record.thy Expressions containing _ and ^ need to be adjusted or antiquoted in text comments for latex compatibility. This is in fact a little annoying, since it makes the comment less readable in both source and HTML form.

Merge record patch with updates from isabelle mainline.

Avoid record-inner constants in polymorphic definitions in Bali The Bali package needs to insert a record extension into a type class and define an associated polymorphic constant. There is no elegant way to do this. The existing approach was to insert every record extension into the type class, defining the polymorphic constant at each layer using inner operations created by the record package. Some of those operations have been removed. They can be replaced by use of record_name.extend if necessary, but we can also sidestep this altogether. The simpler approach here is to use defs(overloaded) once to provide a single definition for the composition of all the type constructors, which seems to be permitted. This gets us exactly the fact we need, with the cost that some types that were admitted to the type class have no definition for the constant at all.