#
7839c3ab |
|
24-Nov-2008 |
Konrad Slind <konrad.slind@gmail.com> |
Fix for a Define bug spotted by mjcg. When dealing with recursive calls under a case, if variables with certain names (those starting with v) are bound in the case pattern then it can happen that variables generated during pattern matching can be the same, leading to failed proofs. Totally obscure, and dealt with properly (I think) in normal pattern matching. So, a difference between Pmatch and Functional. The fix is to invent a class of variables not accepted by the parser (i.e. starting *v) and to later eliminate the weird names from any theorems coming out of Hol_defn. Some other trivial mods made in passing also, plus tests for the new behaviour. Also a new conversional, MAP_THM, which applies the given conversion to the assumptions and conclusion of the given theorem.
|