updating a few of the script commands

Author: mattulbrich

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

@@ -144,9 +144,11 @@ private TacletApp instantiateTacletApp(final Parameters p, final EngineState sta
         ImmutableList<TacletApp> assumesCandidates = theApp
                 .findIfFormulaInstantiations(state.getFirstOpenAutomaticGoal().sequent(), services);
 
-        assumesCandidates = ImmutableList.fromList(filterList(p, assumesCandidates));
+        assumesCandidates = ImmutableList.fromList(filterList(services, p, assumesCandidates));
 
-        if (assumesCandidates.size() != 1) {
+        if (assumesCandidates.size() == 0) {
+            throw new ScriptException("No \\assumes instantiation");
+        } else if (assumesCandidates.size() != 1) {
             throw new ScriptException("Not a unique \\assumes instantiation");
         }
 
@@ -244,7 +246,7 @@ private IBuiltInRuleApp builtInRuleApp(Parameters p, EngineState state, BuiltInR
     private TacletApp findTacletApp(Parameters p, EngineState state) throws ScriptException {
 
         ImmutableList<TacletApp> allApps = findAllTacletApps(p, state);
-        List<TacletApp> matchingApps = filterList(p, allApps);
+        List<TacletApp> matchingApps = filterList(state.getProof().getServices(), p, allApps);
 
         if (matchingApps.isEmpty()) {
             throw new ScriptException("No matching applications.");
@@ -363,7 +365,7 @@ private static String formatTermString(String str) {
     /*
      * Filter those apps from a list that are according to the parameters.
      */
-    private List<TacletApp> filterList(Parameters p, ImmutableList<TacletApp> list) {
+    private List<TacletApp> filterList(Services services, Parameters p, ImmutableList<TacletApp> list) {
         List<TacletApp> matchingApps = new ArrayList<>();
         for (TacletApp tacletApp : list) {
             if (tacletApp instanceof PosTacletApp pta) {