src/Pure/Isar/outer_syntax.scala

         case ((x, y), tok) =>
           if (tok.is_command) {
             if (keywords.is_command(tok, Keyword.theory_goal)) (2, 1)
             else if (keywords.is_command(tok, Keyword.theory)) (1, 0)
             else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1)
-            else if (keywords.is_command(tok, Keyword.PRF_BLOCK == _)) (y + 2, y + 1)
-            else if (keywords.is_command(tok, Keyword.QED_BLOCK == _)) (y - 1, y - 2)
-            else if (keywords.is_command(tok, Keyword.PRF_CLOSE == _)) (y, y - 1)
+            else if (keywords.is_command(tok, Set(Keyword.PRF_BLOCK))) (y + 2, y + 1)
+            else if (keywords.is_command(tok, Set(Keyword.QED_BLOCK))) (y - 1, y - 2)
+            else if (keywords.is_command(tok, Set(Keyword.PRF_CLOSE))) (y, y - 1)
             else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1)
             else if (keywords.is_command(tok, Keyword.qed_global)) (1, 0)
             else (x, y)
           }
           else (x, y)