[isabelle-dev] Problem nach Isabelle Update

[Steven Obua]

Hi,

ich habe gerade Isabelle geupdatet auf meinem Rechner. Leider läuft 
jetzt eine Theorie bei mir nicht mehr durch (und damit auch alles andere 
was ich so für meine tägliche Arbeit brauche :-( )

Und zwar:

Ich lade die Theorie mit 'use_thy "While"'. Nachdem ALLE lemmas in der 
Theorie erfolgreich abgearbeitet wurden, kommt eine exception:

*** exception THM raised: Ill-typed instantiation
Exception- TOPLEVEL_ERROR raised

Es gibt keine ML-files, die noch geladen würden oder so. Im 
Proof-general kann ich die Theorie ohne Probleme durchlaufen lassen.

Irgendwelche Ideen, was da schief laufen könnte?

Steven