fix schiffl_lemma_2

Author: wadoon

key.core/src/main/java/de/uka/ilkd/key/scripts/ProofScriptEngine.java

@@ -137,12 +137,12 @@ public void execute(AbstractUserInterfaceControl uiControl, List<ScriptCommandAs
 
             String cmd = ast.asCommandLine();
 
-            final Node firstNode = stateMap.getFirstOpenAutomaticGoal().node();
-            if (commandMonitor != null && stateMap.isEchoOn()) {
-                commandMonitor.accept(new ExecuteInfo(cmd, start, firstNode.serialNr()));
-            }
-
             try {
+                final Node firstNode = stateMap.getFirstOpenAutomaticGoal().node();
+                if (commandMonitor != null && stateMap.isEchoOn()) {
+                    commandMonitor.accept(new ExecuteInfo(cmd, start, firstNode.serialNr()));
+                }
+
                 ProofScriptCommand command = COMMANDS.get(name);
                 if (command == null) {
                     throw new ScriptException("Unknown command " + name + " at " + ast.location());

key.core/tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof

@@ -404,14 +404,4 @@ instantiate hide var=iv with=(v_y_0);
 instantiate hide var=jv with=(jv_1);
 instantiate hide var=v_r with=(seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1));
 tryclose branch;
-rule seqNPermSwapNPerm formula=(seqNPerm(s_0));
-instantiate hide var=iv with=(v_x_0);
-instantiate hide var=jv with=(jv_0);
-rule impLeft;
-tryclose branch;
-rule seqNPermSwapNPerm formula=(seqNPerm(seqSwap(s_0,v_x_0,jv_0)));
-instantiate hide var=iv with=(v_y_0);
-instantiate hide var=jv with=(jv_1);
-instantiate hide var=v_r with=(seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1));
-tryclose branch;
 }