Re: [isabelle] Loose bound variable



On 18/02/10 16:27, Andreas Lochbihler wrote:
> However, simp (and all methods
> that use the simplifier) produce only this error message:
> 
> *** exception TYPE raised (line 341 of "sign.ML"): Loose bound variable:
> B.4
> *** At command "apply".

Hi Andreas,

thanks for reporting this problem. The exception was caused by a bug in
(r)trancl_tac, which is installed in the simpset as a solver. I have fixed
this in the repository version of Isabelle, see
http://isabelle.in.tum.de/repos/isabelle/rev/206e2f1759cc

Greetings,
Stefan

-- 
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe





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