Sat, 01 Sep 2007 18:17:44 +0200 removed unused join_mode;
wenzelm [Sat, 01 Sep 2007 18:17:44 +0200] rev 24518
removed unused join_mode; standard_typ_check: proper prepare_patternT, which rejects schematic type vars in non-patterns;
Sat, 01 Sep 2007 18:17:42 +0200 read_def_terms: replaced full Syntax.check_typs by certify_typ, to workaround problems with illegal schematic type vars;
wenzelm [Sat, 01 Sep 2007 18:17:42 +0200] rev 24517
read_def_terms: replaced full Syntax.check_typs by certify_typ, to workaround problems with illegal schematic type vars;
Sat, 01 Sep 2007 18:17:40 +0200 removed obsolete ML bindings;
wenzelm [Sat, 01 Sep 2007 18:17:40 +0200] rev 24516
removed obsolete ML bindings;
(0) -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip