src/HOL/Tools/ATP/atp_proof_reconstruct.ML
Mon, 29 Jul 2013 18:06:39 +0200 blanchet avoid duplicating Var when the types do not quite fit -- since this step occurs before type inference
less more (0) -30 -10 -1 tip