2012-04-03 wenzelm 2012-04-03 better drop background syntax if entity depends on parameters; more direct Type_Infer_Context.const_type instead of Syntax.check_term, which expands abbreviations (and potentially more);
2012-03-12 wenzelm 2012-03-12 clarified prepare_positions: always retain source positions to allow using it as formal information, not just markup reports;
2011-11-10 wenzelm 2011-11-10 pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
2011-11-09 wenzelm 2011-11-09 tuned signature; tuned;
2011-06-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript;
2011-04-19 wenzelm 2011-04-19 split Type_Infer into early and late part, after Proof_Context; added Type_Infer_Context.const_sorts option, which allows NBE to use regular Syntax.check_term;