diff -r ade8d65b212e -r 922273b7bf8a src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Mon Aug 11 22:46:27 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Aug 11 22:59:38 2014 +0200
@@ -332,8 +332,8 @@
     val visible = perspective.commands.toSet
 
     def next_invisible_command(cmds: Linear_Set[Command], from: Command): Command =
-      cmds.iterator(from).dropWhile(cmd => !cmd.is_command || visible(cmd))
-        .find(_.is_command) getOrElse cmds.last
+      cmds.iterator(from).dropWhile(cmd => !cmd.is_proper || visible(cmd))
+        .find(_.is_proper) getOrElse cmds.last
 
     @tailrec def recover(cmds: Linear_Set[Command]): Linear_Set[Command] =
       cmds.find(_.is_unparsed) match {