# [isabelle] skip_proofs in Isabelle2012

The skip_proofs option seems to clash with something in Isabelle2012. I'm getting "Messed-up outer syntax for presentation".
Initially I thought this may be a PG problem, but it's not. I tried the following on the tty level:
serenity:~ kleing$ /Applications/Isabelle2012.app/Isabelle/bin/isabelle tty
> val it = (): unit
val commit = fn: unit -> bool
Welcome to Isabelle/HOL (Isabelle2012: May 2012)
> theory X imports Main begin
theory X
> ML "quick_and_dirty := true";
val it = (): unit
> ML "Toplevel.skip_proofs := true";
val it = (): unit
> end;
> theory A imports "~~/src/HOL/Library/List_Prefix" begin
Loading theory "List_Prefix"
*** Messed-up outer syntax for presentation
*** At command "theory"
I'm only seeing the error when I refer to paths explicitly in the import section and Isabelle actually resolves that path. That is, if I manually (in skip_proof mode) step through List_Prefix first and the theory is loaded, the import works fine. (That defeats the purpose of skip_proof mode, of course, because I'm trying to avoid stepping through 30 files and waiting for an hour).
Any ideas?
Cheers,
Gerwin

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