diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Services.java b/key.core/src/main/java/de/uka/ilkd/key/java/Services.java
index a2b285fd1a3..71f21ede6de 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/java/Services.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/java/Services.java
@@ -147,7 +147,6 @@ public Services getOverlay(NamespaceSet namespaces) {
         return result;
     }
 
-
     /**
      * Returns the TypeConverter associated with this Services object.
      */
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/NamespaceSet.java b/key.core/src/main/java/de/uka/ilkd/key/logic/NamespaceSet.java
index b638b7c1b00..f8272e9f478 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/NamespaceSet.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/NamespaceSet.java
@@ -3,7 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.logic;
 
-import java.util.HashMap;
 import java.util.Map;
 
 import de.uka.ilkd.key.java.JavaProgramElement;
@@ -23,8 +22,6 @@ public class NamespaceSet {
     private Namespace<QuantifiableVariable> varNS = new Namespace<>();
     private Namespace<IProgramVariable> progVarNS = new Namespace<>();
     // TODO: Operators should not be local to goals
-    private Map<Pair<Modality.JavaModalityKind, JavaProgramElement>, Modality> operators =
-        new HashMap<>();
     private Namespace<Function> funcNS = new Namespace<>();
     private Namespace<RuleSet> ruleSetNS = new Namespace<>();
     private Namespace<Sort> sortNS = new Namespace<>();
@@ -34,8 +31,7 @@ public NamespaceSet() {
     }
 
     public NamespaceSet(Namespace<QuantifiableVariable> varNS,
-            Map<Pair<Modality.JavaModalityKind, JavaProgramElement>, Modality> operators,
-            Namespace<Function> funcNS,
+                        Namespace<Function> funcNS,
             Namespace<Sort> sortNS, Namespace<RuleSet> ruleSetNS, Namespace<Choice> choiceNS,
             Namespace<IProgramVariable> programVarNS) {
         this.varNS = varNS;
@@ -47,13 +43,13 @@ public NamespaceSet(Namespace<QuantifiableVariable> varNS,
     }
 
     public NamespaceSet copy() {
-        return new NamespaceSet(variables().copy(), new HashMap<>(operators()), functions().copy(),
+        return new NamespaceSet(variables().copy(), functions().copy(),
             sorts().copy(),
             ruleSets().copy(), choices().copy(), programVariables().copy());
     }
 
     public NamespaceSet shallowCopy() {
-        return new NamespaceSet(variables(), operators(), functions(), sorts(), ruleSets(),
+        return new NamespaceSet(variables(), functions(), sorts(), ruleSets(),
             choices(),
             programVariables());
     }
@@ -61,7 +57,7 @@ public NamespaceSet shallowCopy() {
     // TODO MU: Rename into sth with wrap or similar
     public NamespaceSet copyWithParent() {
         return new NamespaceSet(new Namespace<>(variables()),
-            operators(), new Namespace<>(functions()), new Namespace<>(sorts()),
+                new Namespace<>(functions()), new Namespace<>(sorts()),
             new Namespace<>(ruleSets()), new Namespace<>(choices()),
             new Namespace<>(programVariables()));
     }
@@ -82,15 +78,6 @@ public void setProgramVariables(Namespace<IProgramVariable> progVarNS) {
         this.progVarNS = progVarNS;
     }
 
-    public Map<Pair<Modality.JavaModalityKind, JavaProgramElement>, Modality> operators() {
-        return operators;
-    }
-
-    public void setOperators(
-            Map<Pair<Modality.JavaModalityKind, JavaProgramElement>, Modality> operators) {
-        this.operators = operators;
-    }
-
     public Namespace<Function> functions() {
         return funcNS;
     }
@@ -218,12 +205,12 @@ public boolean isEmpty() {
 
     // create a namespace
     public NamespaceSet simplify() {
-        return new NamespaceSet(varNS.simplify(), operators, funcNS.simplify(), sortNS.simplify(),
+        return new NamespaceSet(varNS.simplify(), funcNS.simplify(), sortNS.simplify(),
             ruleSetNS.simplify(), choiceNS.simplify(), progVarNS.simplify());
     }
 
     public NamespaceSet getCompression() {
-        return new NamespaceSet(varNS.compress(), operators, funcNS.compress(), sortNS.compress(),
+        return new NamespaceSet(varNS.compress(), funcNS.compress(), sortNS.compress(),
             ruleSetNS.compress(), choiceNS.compress(), progVarNS.compress());
     }
 
@@ -234,7 +221,7 @@ public void flushToParent() {
     }
 
     public NamespaceSet getParent() {
-        return new NamespaceSet(varNS.parent(), operators, funcNS.parent(), sortNS.parent(),
+        return new NamespaceSet(varNS.parent(), funcNS.parent(), sortNS.parent(),
             ruleSetNS.parent(), choiceNS.parent(), progVarNS.parent());
     }
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java
index b331299efc5..239dfed91fc 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java
@@ -423,12 +423,12 @@ public Term func(Function f, Term[] s, ImmutableArray<QuantifiableVariable> boun
 //    }
 
     public Term prog(Modality.JavaModalityKind modKind, JavaBlock jb, Term t) {
-        return tf.createTerm(modality(modKind, jb), new Term[] { t }, null, jb);
+        return tf.createTerm(Modality.modality(modKind, jb), new Term[] { t }, null, jb);
     }
 
     public Term prog(Modality.JavaModalityKind modKind, JavaBlock jb, Term t,
             ImmutableArray<TermLabel> labels) {
-        return tf.createTerm(modality(modKind, jb), new Term[] { t }, null, jb, labels);
+        return tf.createTerm(Modality.modality(modKind, jb), new Term[] { t }, null, jb, labels);
     }
 
     public Term box(JavaBlock jb, Term t) {
@@ -439,17 +439,6 @@ public Term dia(JavaBlock jb, Term t) {
         return prog(Modality.JavaModalityKind.DIA, jb, t);
     }
 
-    // TODO: move?
-    public Modality modality(Modality.JavaModalityKind kind, JavaBlock jb) {
-        var pair = new Pair<>(kind, jb.program());
-        Modality mod = services.getNamespaces().operators().get(pair);
-        if (mod == null) {
-            mod = new Modality(jb, kind);
-            services.getNamespaces().operators().put(pair, mod);
-        }
-        return mod;
-    }
-
     public Term ife(Term cond, Term _then, Term _else) {
         return tf.createTerm(IfThenElse.IF_THEN_ELSE, cond, _then, _else);
     }
@@ -1706,7 +1695,7 @@ public Term addLabel(Term term, ImmutableArray<TermLabel> labels) {
 
             for (TermLabel newLabel : labels) {
                 for (TermLabel oldLabel : newLabelList) {
-                    if (oldLabel.getClass().equals(newLabel.getClass())) {
+                    if (oldLabel.getClass() == newLabel.getClass()) {
                         newLabelList.remove(oldLabel);
                         break;
                     }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java
index 15544141c0f..17c25cac245 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java
@@ -362,6 +362,10 @@ private boolean unifyHelp(Term t0, Term t1, ImmutableList<QuantifiableVariable>
             return true;
         }
 
+        if (t0.sort() != t1.sort() || t0.arity() != t1.arity()) {
+            return false;
+        }
+
         final Operator op0 = t0.op();
 
         if (op0 instanceof QuantifiableVariable) {
@@ -374,7 +378,7 @@ private boolean unifyHelp(Term t0, Term t1, ImmutableList<QuantifiableVariable>
             if (mod0.kind() != mod1.kind()) {
                 return false;
             }
-            nat = handleJava(t0, t1, nat);
+            nat = handleJava(mod0.program(), mod1.program(), nat);
             if (nat == FAILED) {
                 return false;
             }
@@ -382,16 +386,13 @@ private boolean unifyHelp(Term t0, Term t1, ImmutableList<QuantifiableVariable>
             return false;
         }
 
-        if (t0.sort() != t1.sort() || t0.arity() != t1.arity()) {
-            return false;
-        }
-
-        if (!(t0.op() instanceof SchemaVariable) && t0.op() instanceof ProgramVariable) {
-            if (!(t1.op() instanceof ProgramVariable)) {
-                return false;
-            }
-            nat = checkNat(nat);
-            if (!((ProgramVariable) t0.op()).equalsModRenaming((ProgramVariable) t1.op(), nat)) {
+        if (!(op0 instanceof SchemaVariable) && op0 instanceof ProgramVariable pv0) {
+            if (op1 instanceof ProgramVariable pv1) {
+                nat = checkNat(nat);
+                if (!pv0.equalsModRenaming(pv1, nat)) {
+                    return false;
+                }
+            } else {
                 return false;
             }
         }
@@ -413,15 +414,13 @@ && compareBoundVariables((QuantifiableVariable) t0.op(),
      */
     private static final NameAbstractionTable FAILED = new NameAbstractionTable();
 
-    private static NameAbstractionTable handleJava(Term t0, Term t1, NameAbstractionTable nat) {
-
-        if (!t0.javaBlock().isEmpty() || !t1.javaBlock().isEmpty()) {
+    private static NameAbstractionTable handleJava(JavaBlock jb0, JavaBlock jb1, NameAbstractionTable nat) {
+        if (!jb0.isEmpty() || !jb1.isEmpty()) {
             nat = checkNat(nat);
-            if (!t0.javaBlock().equalsModRenaming(t1.javaBlock(), nat)) {
+            if (!jb0.equalsModRenaming(jb1, nat)) {
                 return FAILED;
             }
         }
-
         return nat;
     }
 
@@ -484,7 +483,9 @@ public boolean equals(Object o) {
         final TermImpl t = (TermImpl) o;
 
         return op.equals(t.op) && t.hasLabels() == hasLabels() && subs.equals(t.subs)
-                && boundVars.equals(t.boundVars) && javaBlock().equals(t.javaBlock());
+                && boundVars.equals(t.boundVars)
+                // TODO (DD): below is no longer necessary
+                && javaBlock().equals(t.javaBlock());
     }
 
     @Override
@@ -709,7 +710,7 @@ public ImmutableArray<TermLabel> getLabels() {
     public boolean containsJavaBlockRecursive() {
         if (containsJavaBlockRecursive == ThreeValuedTruth.UNKNOWN) {
             ThreeValuedTruth result = ThreeValuedTruth.FALSE;
-            if (javaBlock() != null && !javaBlock().isEmpty()) {
+            if (!javaBlock().isEmpty()) {
                 result = ThreeValuedTruth.TRUE;
             } else {
                 for (int i = 0, arity = subs.size(); i < arity; i++) {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Modality.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Modality.java
index b62e1accb2d..6d068010fe1 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Modality.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Modality.java
@@ -6,6 +6,7 @@
 import java.util.HashMap;
 import java.util.Map;
 
+import de.uka.ilkd.key.java.JavaProgramElement;
 import de.uka.ilkd.key.ldt.JavaDLTheory;
 import de.uka.ilkd.key.logic.JavaBlock;
 import de.uka.ilkd.key.logic.Term;
@@ -15,12 +16,37 @@
 
 import org.key_project.logic.Name;
 import org.key_project.logic.Program;
+import org.key_project.util.collection.Pair;
 
 /**
  * This class is used to represent a dynamic logic modality like diamond and box (but also
  * extensions of DL like preserves and throughout are possible in the future).
  */
 public class Modality extends org.key_project.logic.op.Modality<Sort> implements Operator {
+    /*
+       keeps track of created modalities
+     */
+    private static Map<Pair<JavaModalityKind, JavaProgramElement>, Modality> operators =
+            new HashMap<>();
+
+
+    /**
+     * Returns the knownm modalities
+     */
+    public static Map<Pair<JavaModalityKind, JavaProgramElement>, Modality> operators() {
+        return operators;
+    }
+
+    public static Modality modality(Modality.JavaModalityKind kind, JavaBlock jb) {
+        var pair = new Pair<>(kind, jb.program());
+        Modality mod = Modality.operators().get(pair);
+        if (mod == null) {
+            mod = new Modality(jb, kind);
+            Modality.operators().put(pair, mod);
+        }
+        return mod;
+    }
+
     /**
      * creates a modal operator with the given name
      *
@@ -142,7 +168,6 @@ public static class JavaModalityKind extends Kind implements SVSubstitute {
          */
         public static final JavaModalityKind TOUT_TRANSACTION =
             new JavaModalityKind(new Name("throughout_transaction"));
-        public static final JavaModalityKind MOD_SV = new JavaModalityKind(new Name("mod_sv"));
 
         public JavaModalityKind(Name name) {
             super(name);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java
index 90723f4d0e9..4c497f20778 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java
@@ -1151,9 +1151,10 @@ public Object visitModality_term(KeYParser.Modality_termContext ctx) {
              * "No schema elements allowed outside taclet declarations (" + sjb.opName + ")"); }
              */
             Modality.JavaModalityKind kind = (Modality.JavaModalityKind) schemaVariables().lookup(new Name(sjb.opName));
-            op = getServices().getTermBuilder().modality(kind, sjb.javaBlock);
+            op = Modality.modality(kind, sjb.javaBlock);
         } else {
-            op = getServices().getTermBuilder().modality(Modality.JavaModalityKind.getKind(sjb.opName), sjb.javaBlock);
+            Modality.JavaModalityKind kind = Modality.JavaModalityKind.getKind(sjb.opName);
+            op = Modality.modality(kind, sjb.javaBlock);
         }
         if (op == null) {
             semanticError(ctx, "Unknown modal operator: " + sjb.opName);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java b/key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java
index 21b1821a355..b30457707af 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java
@@ -5,9 +5,7 @@
 
 import java.io.IOException;
 import java.io.Reader;
-import java.util.Map;
 
-import de.uka.ilkd.key.java.JavaProgramElement;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.Namespace;
 import de.uka.ilkd.key.logic.NamespaceSet;
@@ -15,14 +13,11 @@
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.op.Function;
 import de.uka.ilkd.key.logic.op.IProgramVariable;
-import de.uka.ilkd.key.logic.op.Modality;
 import de.uka.ilkd.key.logic.op.QuantifiableVariable;
 import de.uka.ilkd.key.logic.sort.Sort;
 import de.uka.ilkd.key.nparser.KeyIO;
 import de.uka.ilkd.key.pp.AbbrevMap;
 
-import org.key_project.util.collection.Pair;
-
 import org.antlr.v4.runtime.CharStreams;
 import org.antlr.v4.runtime.RecognitionException;
 
@@ -42,18 +37,16 @@ public final class DefaultTermParser {
      * ensures, that the term has the specified sort.
      *
      * @param sort The expected sort of the term.
-     * @param op_ns
      * @return The parsed term of the specified sort.
      * @throws ParserException The method throws a ParserException, if the input could not be parsed
-     *         correctly or the term has an invalid sort.
+     *                         correctly or the term has an invalid sort.
      */
     public Term parse(Reader in, Sort sort, Services services,
             Namespace<QuantifiableVariable> var_ns,
-            Map<Pair<Modality.JavaModalityKind, JavaProgramElement>, Modality> op_ns,
-            Namespace<Function> func_ns,
+                      Namespace<Function> func_ns,
             Namespace<Sort> sort_ns, Namespace<IProgramVariable> progVar_ns, AbbrevMap scm)
             throws ParserException {
-        return parse(in, sort, services, new NamespaceSet(var_ns, op_ns, func_ns, sort_ns,
+        return parse(in, sort, services, new NamespaceSet(var_ns, func_ns, sort_ns,
             new Namespace<>(), new Namespace<>(), progVar_ns), scm);
     }
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java
index 7ba2a16dbac..1399739e77f 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java
@@ -1667,7 +1667,8 @@ public void printModalityTerm(String left, JavaBlock jb, String right, Term phi,
                     for (int i = 0; i < phi.arity(); i++) {
                         ta[i] = phi.sub(i);
                     }
-                    Modality m = services.getTermBuilder().modality(mod.kind(), mod.program());
+                    JavaBlock jb1 = mod.program();
+                    Modality m = Modality.modality(mod.kind(), jb1);
                     Term term = services.getTermFactory().createTerm(m, ta,
                         phi.boundVars(), phi.javaBlock());
                     notationInfo.getNotation(m).print(term, this);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java
index f0eb999cd46..ae4e73bc0ce 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java
@@ -468,11 +468,10 @@ private GoalsConfigurator setUpGoalConfigurator(final StatementBlock block,
         final KeYJavaType kjt = getCalleeKeYJavaType();
         final TypeRef typeRef = new TypeRef(new ProgramElementName(kjt.getName()), 0, selfVar, kjt);
         final ExecutionContext ec = new ExecutionContext(typeRef, getProgramMethod(), selfVar);
-        // TODO (DD): HACK
         final Instantiation inst =
             new Instantiation(tb.skip(), tb.tt(),
-                new Modality(JavaBlock.createJavaBlock(new StatementBlock()),
-                    contract.getModalityKind()),
+                Modality.modality(contract.getModalityKind(),
+                        JavaBlock.createJavaBlock(new StatementBlock())),
                 selfTerm, block, ec);
         return new GoalsConfigurator(null, new TermLabelState(), inst,
             contract.getAuxiliaryContract().getLabels(), variables, null, services, null);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java
index 33e9fed35cf..b2b3f774684 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java
@@ -940,7 +940,7 @@ public static Term parseTerm(String value, Proof proof, Namespace<QuantifiableVa
             Namespace<IProgramVariable> progVarNS, Namespace<Function> functNS) {
         try {
             return new DefaultTermParser().parse(new StringReader(value), null, proof.getServices(),
-                varNS, proof.getNamespaces().operators(), functNS, proof.getNamespaces().sorts(),
+                varNS, functNS, proof.getNamespaces().sorts(),
                 progVarNS, new AbbrevMap());
         } catch (ParserException e) {
             throw new RuntimeException(
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/LightweightSyntacticalReplaceVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/rule/LightweightSyntacticalReplaceVisitor.java
index 08856806300..285e50a2e3c 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/LightweightSyntacticalReplaceVisitor.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/LightweightSyntacticalReplaceVisitor.java
@@ -156,11 +156,18 @@ private ElementaryUpdate instantiateElementaryUpdate(ElementaryUpdate op) {
         }
     }
 
-    private Operator instantiateOperatorSV(ModalOperatorSV op) {
-        return (Operator) svInst.getInstantiation(op);
+    private Operator instantiateModality(Modality op, JavaBlock jb) {
+        Modality.JavaModalityKind kind = op.kind();
+        if (op.kind() instanceof ModalOperatorSV) {
+            kind = (Modality.JavaModalityKind) svInst.getInstantiation(op.kind());
+        }
+        if (jb != op.program() || kind != op.kind()) {
+            return Modality.modality(kind, jb);
+        }
+        return op;
     }
 
-    private Operator instantiateOperator(Operator p_operatorToBeInstantiated) {
+    protected Operator instantiateOperator(Operator p_operatorToBeInstantiated, JavaBlock jb) {
         Operator instantiatedOp = p_operatorToBeInstantiated;
         if (p_operatorToBeInstantiated instanceof SortDependingFunction) {
             instantiatedOp =
@@ -168,8 +175,8 @@ private Operator instantiateOperator(Operator p_operatorToBeInstantiated) {
         } else if (p_operatorToBeInstantiated instanceof ElementaryUpdate) {
             instantiatedOp =
                 instantiateElementaryUpdate((ElementaryUpdate) p_operatorToBeInstantiated);
-        } else if (p_operatorToBeInstantiated instanceof ModalOperatorSV) {
-            instantiatedOp = instantiateOperatorSV((ModalOperatorSV) p_operatorToBeInstantiated);
+        } else if (p_operatorToBeInstantiated instanceof Modality mod) {
+            instantiatedOp = instantiateModality(mod, jb);
         } else if (p_operatorToBeInstantiated instanceof SchemaVariable) {
             if (p_operatorToBeInstantiated instanceof ProgramSV
                     && ((ProgramSV) p_operatorToBeInstantiated).isListSV()) {
@@ -227,7 +234,6 @@ public void visit(final Term visited) {
                 svInst.getExecutionContext(), services));
             pushNew(newTerm);
         } else {
-            final Operator newOp = instantiateOperator(visitedOp);
             // instantiation of java block
             boolean jblockChanged = false;
             JavaBlock jb = visited.javaBlock();
@@ -239,6 +245,8 @@ public void visit(final Term visited) {
                 }
             }
 
+            final Operator newOp = instantiateOperator(visitedOp, jb);
+
             // instantiate bound variables
             final ImmutableArray<QuantifiableVariable> boundVars = //
                 instantiateBoundVariables(visited);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java
index c78221b2ad8..aaed147d42b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java
@@ -219,7 +219,7 @@ private Operator instantiateModality(Modality op, JavaBlock jb) {
             kind = (Modality.JavaModalityKind) svInst.getInstantiation(op.kind());
         }
         if (jb != op.program() || kind != op.kind()) {
-            return tb.modality(kind, jb);
+            return Modality.modality(kind, jb);
         }
         return op;
     }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java
index f2051cd6fbb..3c1751456e3 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java
@@ -59,11 +59,11 @@ public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate,
                 .map(methodFrame -> MiscTools.getSelfTerm(methodFrame, services)).orElse(null);
 
         // TODO: handle exception!
-        final Modality modality = (Modality) svInst.getInstantiation(modalitySV);
+        final Modality.JavaModalityKind modalityKind =
+                (Modality.JavaModalityKind) svInst.getInstantiation(modalitySV);
 
         boolean hasInv = false;
-        for (final LocationVariable heap : MiscTools.applicableHeapContexts(modality.kind(),
-            services)) {
+        for (final LocationVariable heap : MiscTools.applicableHeapContexts(modalityKind, services)) {
             final Optional<Term> maybeInvInst = Optional.ofNullable(
                 loopSpec.getInvariant(heap, selfTerm, loopSpec.getInternalAtPres(), services));
             final Optional<Term> maybeFreeInvInst = Optional.ofNullable(
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java
index 4094f2d2838..669d34e3af6 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java
@@ -68,10 +68,10 @@ public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate,
                 .map(methodFrame -> MiscTools.getSelfTerm(methodFrame, services)).orElse(null);
 
         // TODO: Handle exception?!
-        final Modality modality = (Modality) svInst.getInstantiation(modalitySV);
+        final Modality.JavaModalityKind modalityKind = (Modality.JavaModalityKind) svInst.getInstantiation(modalitySV);
 
         Term freeInvInst = tb.tt();
-        for (final LocationVariable heap : MiscTools.applicableHeapContexts(modality.kind(),
+        for (final LocationVariable heap : MiscTools.applicableHeapContexts(modalityKind,
             services)) {
             final Term currentFreeInvInst = freeInvInst;
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java
index 82e8d3ecc36..91007b728e5 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java
@@ -68,10 +68,11 @@ public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate,
                 .map(methodFrame -> MiscTools.getSelfTerm(methodFrame, services)).orElse(null);
 
         // TODO: handle exception
-        final Modality modality = (Modality) svInst.getInstantiation(modalitySV);
+        final Modality.JavaModalityKind modalityKind =
+                (Modality.JavaModalityKind) svInst.getInstantiation(modalitySV);
 
         Term invInst = tb.tt();
-        for (final LocationVariable heap : MiscTools.applicableHeapContexts(modality.kind(),
+        for (final LocationVariable heap : MiscTools.applicableHeapContexts(modalityKind,
             services)) {
             final Term currentInvInst = invInst;
 
diff --git a/key.core/src/test/java/de/uka/ilkd/key/logic/TestTerm.java b/key.core/src/test/java/de/uka/ilkd/key/logic/TestTerm.java
index 7e52795f228..1f5ed6fed60 100644
--- a/key.core/src/test/java/de/uka/ilkd/key/logic/TestTerm.java
+++ b/key.core/src/test/java/de/uka/ilkd/key/logic/TestTerm.java
@@ -194,7 +194,7 @@ public void testIsContainsJavaBlockRecursive() {
         Term noJBWithChild = tf.createTerm(Junctor.NOT, noJB);
         JavaBlock javaBlock =
             JavaBlock.createJavaBlock(new StatementBlock(new LocalVariableDeclaration()));
-        Term withJB = tf.createTerm(tb.modality(Modality.JavaModalityKind.DIA, javaBlock), new ImmutableArray<>(noJB), null, javaBlock);
+        Term withJB = tf.createTerm(Modality.modality(Modality.JavaModalityKind.DIA, javaBlock), new ImmutableArray<>(noJB), null, javaBlock);
         Term withJBChild = tf.createTerm(Junctor.NOT, withJB);
         Term withJBChildChild = tf.createTerm(Junctor.NOT, withJBChild);
         assertFalse(noJB.containsJavaBlockRecursive());
diff --git a/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermFactory.java b/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermFactory.java
index 6108f906963..072297ea151 100644
--- a/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermFactory.java
+++ b/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermFactory.java
@@ -166,15 +166,15 @@ public void testNegationTerm() {
     @Test
     public void testDiamondTerm() {
         JavaBlock jb = JavaBlock.EMPTY_JAVABLOCK;
-        Term t_dia_ryw = tf.createTerm(TB.modality(Modality.JavaModalityKind.DIA, jb), new Term[] { t2() }, null, jb);
-        assertEquals(t_dia_ryw, new TermImpl(TB.modality(Modality.JavaModalityKind.DIA, jb), new ImmutableArray<>(t2()), null, jb));
+        Term t_dia_ryw = tf.createTerm(Modality.modality(Modality.JavaModalityKind.DIA, jb), new Term[] { t2() }, null, jb);
+        assertEquals(t_dia_ryw, new TermImpl(Modality.modality(Modality.JavaModalityKind.DIA, jb), new ImmutableArray<>(t2()), null, jb));
     }
 
     @Test
     public void testBoxTerm() {
         JavaBlock jb = JavaBlock.EMPTY_JAVABLOCK;
-        Term t_dia_ryw = tf.createTerm(TB.modality(Modality.JavaModalityKind.BOX, jb), new ImmutableArray<>(t2()), null, jb);
-        assertEquals(t_dia_ryw, new TermImpl(TB.modality(Modality.JavaModalityKind.BOX, jb), new ImmutableArray<>(t2()), null, jb));
+        Term t_dia_ryw = tf.createTerm(Modality.modality(Modality.JavaModalityKind.BOX, jb), new ImmutableArray<>(t2()), null, jb);
+        assertEquals(t_dia_ryw, new TermImpl(Modality.modality(Modality.JavaModalityKind.BOX, jb), new ImmutableArray<>(t2()), null, jb));
     }
 
     @Test
@@ -319,7 +319,7 @@ public void testCaching() {
         Term noJBWithChild = tf.createTerm(Junctor.NOT, noJB);
         JavaBlock javaBlock =
             JavaBlock.createJavaBlock(new StatementBlock(new LocalVariableDeclaration()));
-        Term withJB = tf.createTerm(TB.modality(Modality.JavaModalityKind.DIA, javaBlock), new ImmutableArray<>(noJB), null, javaBlock);
+        Term withJB = tf.createTerm(Modality.modality(Modality.JavaModalityKind.DIA, javaBlock), new ImmutableArray<>(noJB), null, javaBlock);
         Term withJBChild = tf.createTerm(Junctor.NOT, withJB);
         Term withJBChildChild = tf.createTerm(Junctor.NOT, withJBChild);
         // Create Same terms again
@@ -328,7 +328,7 @@ public void testCaching() {
         JavaBlock javaBlockAgain =
             JavaBlock.createJavaBlock(new StatementBlock(new LocalVariableDeclaration()));
         Term withJBAgain =
-            tf.createTerm(TB.modality(Modality.JavaModalityKind.DIA, javaBlockAgain), new ImmutableArray<>(noJB), null, javaBlockAgain);
+            tf.createTerm(Modality.modality(Modality.JavaModalityKind.DIA, javaBlockAgain), new ImmutableArray<>(noJB), null, javaBlockAgain);
         Term withJBChildAgain = tf.createTerm(Junctor.NOT, withJB);
         Term withJBChildChildAgain = tf.createTerm(Junctor.NOT, withJBChild);
         // Test caching
diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/TestSchemaModalOperators.java b/key.core/src/test/java/de/uka/ilkd/key/rule/TestSchemaModalOperators.java
index d62c22e59bc..f8d961c7388 100644
--- a/key.core/src/test/java/de/uka/ilkd/key/rule/TestSchemaModalOperators.java
+++ b/key.core/src/test/java/de/uka/ilkd/key/rule/TestSchemaModalOperators.java
@@ -124,10 +124,10 @@ public void testSchemaModalities1() {
             JavaDLTheory.FORMULA, modalities);
         Term tpost = TB.tf().createTerm(fsv);
 
-        Term find = TB.tf().createTerm(TB.modality((Modality.JavaModalityKind) osv, JavaBlock.EMPTY_JAVABLOCK), new Term[] { tpost }, null, JavaBlock.EMPTY_JAVABLOCK);
+        Term find = TB.tf().createTerm(Modality.modality((Modality.JavaModalityKind) osv, JavaBlock.EMPTY_JAVABLOCK), new Term[] { tpost }, null, JavaBlock.EMPTY_JAVABLOCK);
 
         Term replace =
-            TB.tf().createTerm(TB.modality((Modality.JavaModalityKind) osv, JavaBlock.EMPTY_JAVABLOCK), new Term[] { TB.tt() }, null, JavaBlock.EMPTY_JAVABLOCK);
+            TB.tf().createTerm(Modality.modality((Modality.JavaModalityKind) osv, JavaBlock.EMPTY_JAVABLOCK), new Term[] { TB.tt() }, null, JavaBlock.EMPTY_JAVABLOCK);
 
         rtb.setName(new Name("test_schema_modal1"));
         rtb.setFind(find);
diff --git a/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TestTriggersSet.java b/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TestTriggersSet.java
index 361bd9e554b..2bc02886027 100644
--- a/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TestTriggersSet.java
+++ b/key.core/src/test/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TestTriggersSet.java
@@ -18,8 +18,6 @@
 import org.junit.jupiter.api.Disabled;
 import org.junit.jupiter.api.Test;
 
-import java.util.HashMap;
-
 import static org.junit.jupiter.api.Assertions.assertEquals;
 
 
@@ -193,13 +191,13 @@ public void setUp() {
         proof.setRoot(g.node());
         proof.add(g);
 
-        proof.setNamespaces(new NamespaceSet(variables, new HashMap<>(), functions, sorts, new Namespace<>(),
+        proof.setNamespaces(new NamespaceSet(variables, functions, sorts, new Namespace<>(),
             new Namespace<>(), new Namespace<>()));
 
     }
 
     private Term parseTerm(String termstr) {
-        return TacletForTests.parseTerm(termstr, new NamespaceSet(variables, new HashMap<>(), functions, sorts,
+        return TacletForTests.parseTerm(termstr, new NamespaceSet(variables, functions, sorts,
             new Namespace<>(), new Namespace<>(), new Namespace<>()));
     }