[isabelle-dev] NEWS: type-inference for object-logic

[Makarius]

On Tue, 12 Apr 2016, Peter Lammich wrote:

> so we're not going to see the annoying "... not of sort 'type'" error 
> any more, which used to occur occasionally in Isabelle/HOL 
> developments!?

Yes, but old tools may get broken, if slightly more general types are 
expected. E.g. see the record simprocs in 
http://isabelle.in.tum.de/repos/isabelle/diff/b41c1cb5e251/src/HOL/Tools/record.ML


 	Makarius