[isabelle] Blast behaves strangely with free schematic variables

I downloaded Isabelle2005 just now following the installation
instructions at


and if I start my "ToyList.thy" file with

   theory ToyList
   imports PreList

   lemma bug: "?A & ?B & ?XYZZY \<longrightarrow> ?XYZZY" by blast

and go to the end and press control-c control-enter, I see this in the
response window:

   lemma bug: ?A & ?B & gcd (?m, ?n) dvd ?n --> gcd (?m, ?n) dvd ?n

I had expected it to say:

   lemma bug: ?A & ?B & ?XYZZY --> ?XYZZY

I was surprised by the intruction of the "gcd" operator. If I change
"blast" to "auto", I do get the output I expected.

Tim Freeman               http://www.fungible.com           tim at fungible.com
Pass it on: The Integral Fast Reactor can provide safe, clean
energy.  Politically motivated misrepresentation stopped the research.
Check it out at: http://en.wikipedia.org/wiki/Integral_Fast_Reactor

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.