Thank you for looking there! This is the most plausible culprit. But it is strange that this problem has arisen before.
A possible fix is to replace the last line of the function timing_depth_tac in that file as follows: handle PROVE => Seq.empty | THM _ => Seq.empty; Andreas, do you want to try this and see if it helps? Larry On 27 May 2011, at 15:27, Stefan Berghofer wrote: > Hi Larry and Andreas, > > there is another occurrence of gconv_rule in Provers/blast.ML > (in function timing_depth_tac). Since the exception is thrown > when invoking blast, this occurrence of gconv_rule may be the > culprit. _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
