blanchet [Fri, 14 May 2010 11:23:42 +0200] rev 36909
made Sledgehammer's full-typed proof reconstruction work for the first time;
previously, Isar proofs and full-type mode were mutually exclusive because both options were hard-coded in the ATP names (e.g., "e_isar" and "full_vampire") -- making the options orthogonal revealed that some code was missing to handle types in the proof reconstruction code