diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md
index 8a7c691ac18..72df2bc186c 100644
--- a/k-distribution/include/kframework/builtin/domains.md
+++ b/k-distribution/include/kframework/builtin/domains.md
@@ -2315,14 +2315,9 @@ It is not recommended to use any of them directly as they are largely
 unsupported in modern K. There are a few exceptions:
 
 * `#getenv` - Returns the value of an environment variable
-* `#parseKORE` - Takes a String containing a K intermediate representation of
-  a term such as is returned by `kast -o kore` and converts it to a term.
-  This is NOT type-safe. The responsibility is on the user to ensure that the
-  string they provide is a valid representation of a term of the sort *exactly*
-  equal to the sort where the function appears.
 * `#kompiledDirectory` - Returns the path to the current compiled K definition
   directory.
-* `#unparseKORE` = Takes a K term and converts it to a string.
+* `#unparseKORE` - Takes a K term and converts it to a string.
 
 ```k
 module K-REFLECTION
@@ -2342,8 +2337,6 @@ module K-REFLECTION
   // undefined
   syntax List ::= #argv() [function, hook(KREFLECTION.argv)]
 
-  // Takes as input a string and returns a K term
-  syntax {Sort} Sort ::= #parseKORE(String) [function, hook(KREFLECTION.parseKORE)]
   syntax {Sort} String ::= #unparseKORE(Sort) [function, hook(KREFLECTION.printKORE)]
   syntax IOError ::= "#noParse" "(" String ")" [klabel(#noParse), symbol]
 
diff --git a/k-distribution/tests/regression-new/coverage-poly/1.test b/k-distribution/tests/regression-new/coverage-poly/1.test
deleted file mode 100644
index 7b8a2fbb8e5..00000000000
--- a/k-distribution/tests/regression-new/coverage-poly/1.test
+++ /dev/null
@@ -1 +0,0 @@
-parseFoo()
diff --git a/k-distribution/tests/regression-new/coverage-poly/1.test.out b/k-distribution/tests/regression-new/coverage-poly/1.test.out
deleted file mode 100644
index 12f27dd34b0..00000000000
--- a/k-distribution/tests/regression-new/coverage-poly/1.test.out
+++ /dev/null
@@ -1,3 +0,0 @@
-<k>
-  foo ( ) ~> .
-</k>
diff --git a/k-distribution/tests/regression-new/coverage-poly/Makefile b/k-distribution/tests/regression-new/coverage-poly/Makefile
deleted file mode 100644
index 5a5caf90244..00000000000
--- a/k-distribution/tests/regression-new/coverage-poly/Makefile
+++ /dev/null
@@ -1,6 +0,0 @@
-DEF=test
-EXT=test
-TESTDIR=.
-KOMPILE_FLAGS=--coverage --syntax-module TEST
-
-include ../../../include/kframework/ktest.mak
diff --git a/k-distribution/tests/regression-new/coverage-poly/test.k b/k-distribution/tests/regression-new/coverage-poly/test.k
deleted file mode 100644
index 0918ae5b50e..00000000000
--- a/k-distribution/tests/regression-new/coverage-poly/test.k
+++ /dev/null
@@ -1,8 +0,0 @@
-// Copyright (c) K Team. All Rights Reserved.
-module TEST
-  imports K-REFLECTION
-
-  syntax Foo ::= parseFoo() [function]
-  rule parseFoo() => #parseKORE("Lblfoo{}()")
-  syntax Foo ::= foo() [symbol]
-endmodule
diff --git a/k-distribution/tests/regression-new/parseKORE/1.test b/k-distribution/tests/regression-new/parseKORE/1.test
deleted file mode 100644
index 573541ac970..00000000000
--- a/k-distribution/tests/regression-new/parseKORE/1.test
+++ /dev/null
@@ -1 +0,0 @@
-0
diff --git a/k-distribution/tests/regression-new/parseKORE/1.test.out b/k-distribution/tests/regression-new/parseKORE/1.test.out
deleted file mode 100644
index 63158b6047e..00000000000
--- a/k-distribution/tests/regression-new/parseKORE/1.test.out
+++ /dev/null
@@ -1,8 +0,0 @@
-<generatedTop>
-  <k>
-    1 ~> .
-  </k>
-  <state>
-    abc ( 1 )
-  </state>
-</generatedTop>
diff --git a/k-distribution/tests/regression-new/parseKORE/Makefile b/k-distribution/tests/regression-new/parseKORE/Makefile
deleted file mode 100644
index 86158b0f8d9..00000000000
--- a/k-distribution/tests/regression-new/parseKORE/Makefile
+++ /dev/null
@@ -1,6 +0,0 @@
-DEF=test
-EXT=test
-TESTDIR=.
-KOMPILE_FLAGS=--syntax-module TEST
-
-include ../../../include/kframework/ktest.mak
diff --git a/k-distribution/tests/regression-new/parseKORE/test.k b/k-distribution/tests/regression-new/parseKORE/test.k
deleted file mode 100644
index 3c7f7ae1ae8..00000000000
--- a/k-distribution/tests/regression-new/parseKORE/test.k
+++ /dev/null
@@ -1,12 +0,0 @@
-// Copyright (c) K Team. All Rights Reserved.
-module TEST
-  imports DOMAINS
-  imports K-REFLECTION
-
-  syntax Exp ::= abc(Int) [klabel(abc), symbol]
-
-  configuration <k> $PGM:K </k> <state> #parseKORE("Lblabc{}(\\dv{SortInt{}}(\"1\"))"):Exp </state>
-
-  rule <k> 0 => 1 </k> <state> abc(1) </state>
-
-endmodule
diff --git a/k-distribution/tests/regression-new/parseKORE2/Makefile b/k-distribution/tests/regression-new/parseKORE2/Makefile
deleted file mode 100644
index 7545c609640..00000000000
--- a/k-distribution/tests/regression-new/parseKORE2/Makefile
+++ /dev/null
@@ -1,7 +0,0 @@
-DEF=test
-EXT=test
-KOMPILE_FLAGS=--syntax-module TEST
-
-include ../../../include/kframework/ktest.mak
-krun: kompile
-	$(KRUN_OR_LEGACY) $(KRUN_FLAGS) $(DEBUG) --definition $(DEF)-kompiled $(CHECK) output
diff --git a/k-distribution/tests/regression-new/parseKORE2/output b/k-distribution/tests/regression-new/parseKORE2/output
deleted file mode 100644
index f91de778ab2..00000000000
--- a/k-distribution/tests/regression-new/parseKORE2/output
+++ /dev/null
@@ -1,3 +0,0 @@
-<k>
-  2 ~> .
-</k>
diff --git a/k-distribution/tests/regression-new/parseKORE2/test.k b/k-distribution/tests/regression-new/parseKORE2/test.k
deleted file mode 100644
index 9ec1590357a..00000000000
--- a/k-distribution/tests/regression-new/parseKORE2/test.k
+++ /dev/null
@@ -1,8 +0,0 @@
-// Copyright (c) K Team. All Rights Reserved.
-module TEST
-  imports K-REFLECTION
-  imports INT
-  configuration <k> #parseKORE("\\dv{SortInt{}}(\"1\")"):Int </k>
-
-  rule 1 => 2
-endmodule