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 4602204a73..92230ca0a0 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
@@ -936,19 +936,32 @@ && getNotationInfo().isHidePackagePrefix()) {
         } else {
             String name = t.op().name().toString();
             layouter.startTerm(t.arity());
-            boolean alreadyPrinted = false;
+
             if (t.op() instanceof SortDependingFunction op) {
-                if (op.getKind().compareTo(JavaDLTheory.EXACT_INSTANCE_NAME) == 0) {
-                    layouter.print(op.getSortDependingOn().declarationString());
+
+                // remove package prefix from SortDependingFunction
+                if (notationInfo.isHidePackagePrefix()) {
+                    String sort = op.getSortDependingOn().declarationString();
+                    int index = sort.lastIndexOf('.');
+                    sort = sort.substring(index + 1);
+                    layouter.print(sort);
                     layouter.print("::");
-                    layouter.keyWord(op.getKind().toString());
-                    alreadyPrinted = true;
+
+                    name = op.getKind().toString();
+                }
+
+                // mark instance and exactInstance as keywords
+                if (op.getKind().compareTo(JavaDLTheory.EXACT_INSTANCE_NAME) == 0
+                        || op.getKind().compareTo(JavaDLTheory.INSTANCE_NAME) == 0) {
+                    isKeyword = true;
                 }
             }
             if (isKeyword) {
                 layouter.markStartKeyword();
             }
-            if (!alreadyPrinted) {
+            if (isKeyword) {
+                layouter.keyWord(name);
+            } else {
                 layouter.print(name);
             }
             if (isKeyword) {
@@ -980,7 +993,13 @@ public void printCast(String pre, String post, JTerm t, int ass) {
 
         layouter.startTerm(t.arity());
         layouter.print(pre);
-        layouter.print(cast.getSortDependingOn().toString());
+        String sort = cast.getSortDependingOn().toString();
+        // remove package prefix from sort name
+        if (notationInfo.isHidePackagePrefix()) {
+            int index = sort.lastIndexOf('.');
+            sort = sort.substring(index + 1);
+        }
+        layouter.print(sort);
         layouter.print(post);
         maybeParens(t.sub(0), ass);
     }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java b/key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java
index e124f39f0c..cd99da9ce4 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java
@@ -11,6 +11,7 @@
 import de.uka.ilkd.key.ldt.*;
 import de.uka.ilkd.key.logic.label.TermLabel;
 import de.uka.ilkd.key.logic.op.*;
+import de.uka.ilkd.key.settings.ProofIndependentSettings;
 import de.uka.ilkd.key.settings.ProofSettings;
 import de.uka.ilkd.key.util.UnicodeHelper;
 
@@ -420,7 +421,8 @@ public void refresh(Services services, boolean usePrettyPrinting, boolean useUni
         } else {
             this.notationTable = createDefaultNotation();
         }
-        hidePackagePrefix = DEFAULT_HIDE_PACKAGE_PREFIX;
+        ProofIndependentSettings pis = ProofIndependentSettings.DEFAULT_INSTANCE;
+        hidePackagePrefix = pis.getViewSettings().isHidePackagePrefix();
 
         if (services != null && services.getProof() != null) {
             ProofSettings settings = services.getProof().getSettings();
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/HTMLSyntaxHighlighter.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/HTMLSyntaxHighlighter.java
index 6ddea51c6e..8fb30c3d64 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/HTMLSyntaxHighlighter.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/HTMLSyntaxHighlighter.java
@@ -76,8 +76,8 @@ public class HTMLSyntaxHighlighter {
 
     private final static String[] DYNAMIC_LOGIC_KEYWORDS =
         { "\\forall", "\\exists", "TRUE", "FALSE", "\\if", "\\then", "\\else", "\\sum", "bsum",
-            "\\in", "exactInstance", "wellFormed", "measuredByEmpty", "<created>", "<inv>", "\\cup",
-            "" + FORALL, "" + EXISTS, "" + IN, "" + EMPTY };
+            "\\in", "instance", "exactInstance", "wellFormed", "measuredByEmpty", "<created>",
+            "<inv>", "\\cup", "" + FORALL, "" + EXISTS, "" + IN, "" + EMPTY };
 
     private final static String DYNAMIC_LOGIC_KEYWORDS_REGEX =
         concat("|", Arrays.asList(DYNAMIC_LOGIC_KEYWORDS), input -> Pattern.quote((String) input));