diff --git a/k-distribution/tests/regression-new/bison-glr-bug/iele.k b/k-distribution/tests/regression-new/bison-glr-bug/iele.k
index 042f2984a55..bddfc0530d4 100644
--- a/k-distribution/tests/regression-new/bison-glr-bug/iele.k
+++ b/k-distribution/tests/regression-new/bison-glr-bug/iele.k
@@ -76,7 +76,7 @@ module IELE-COMMON
syntax IeleName ::=
IeleNameToken
syntax IeleName ::=
- StringIeleName [avoid, function, klabel(StringIeleName), symbol]
+ StringIeleName [avoid, function, symbol(StringIeleName)]
syntax GlobalName ::=
"@" IeleName
syntax LocalName ::=
diff --git a/k-distribution/tests/regression-new/checkWarns/missingKlabel.k b/k-distribution/tests/regression-new/checkWarns/missingKlabel.k
index 4ce27642627..7ec6dbbb179 100644
--- a/k-distribution/tests/regression-new/checkWarns/missingKlabel.k
+++ b/k-distribution/tests/regression-new/checkWarns/missingKlabel.k
@@ -7,10 +7,10 @@ module MISSINGKLABEL
imports BASIC-K
syntax MyMap ::= KItem "M|->" KItem
- [ function, total, hook(MAP.element), klabel(_M|->_), symbol, injective, unused]
+ [ function, total, hook(MAP.element), symbol(_M|->_), injective, unused]
syntax MyMap ::= MyMap MyMap
- [ left, function, hook(MAP.concat), klabel(_MyMap_), symbol, assoc, comm
+ [ left, function, hook(MAP.concat), symbol(_MyMap_), assoc, comm
, unit(.MyMap), element(_M|->_), index(0), format(%1%n%2), unused
]
diff --git a/k-distribution/tests/regression-new/context-alias-2/test.k b/k-distribution/tests/regression-new/context-alias-2/test.k
index c7236c77caa..1ed5ccc42a6 100644
--- a/k-distribution/tests/regression-new/context-alias-2/test.k
+++ b/k-distribution/tests/regression-new/context-alias-2/test.k
@@ -8,7 +8,7 @@ module TEST
| Id "=" Int
| Id
| Int
- | l(Exp) [klabel(l), symbol] | m(Exp) [klabel(m), symbol] | r(Exp) [klabel(r), symbol]
+ | l(Exp) [symbol(l)] | m(Exp) [symbol(m)] | r(Exp) [symbol(r)]
syntax KResult ::= Int
context alias [left]: HERE [context(l)]
diff --git a/k-distribution/tests/regression-new/issue-1263/test.k b/k-distribution/tests/regression-new/issue-1263/test.k
index 11116707f64..cf4af38df5b 100644
--- a/k-distribution/tests/regression-new/issue-1263/test.k
+++ b/k-distribution/tests/regression-new/issue-1263/test.k
@@ -5,7 +5,7 @@ module TEST
configuration $PGM:Pgm
- syntax FInt ::= FInt ( value: Int , one: Int ) [klabel(FInt), symbol]
+ syntax FInt ::= FInt ( value: Int , one: Int ) [symbol(FInt)]
// ---------------------------------------------------------------------
syntax Wad = FInt
diff --git a/k-distribution/tests/regression-new/issue-1273/test.k b/k-distribution/tests/regression-new/issue-1273/test.k
index 28d7244cd37..482aae99003 100644
--- a/k-distribution/tests/regression-new/issue-1273/test.k
+++ b/k-distribution/tests/regression-new/issue-1273/test.k
@@ -4,7 +4,7 @@ module TEST
imports BOOL
syntax FInt ::= "(" FInt ")" [bracket]
- | FInt ( value: Int , one: Int ) [klabel(FInt), symbol]
+ | FInt ( value: Int , one: Int ) [symbol(FInt)]
// ---------------------------------------------------------------------
syntax FInt ::= "1FInt" "(" Int ")" [macro]
diff --git a/k-distribution/tests/regression-new/issue-1682-korePrettyPrint/test.k b/k-distribution/tests/regression-new/issue-1682-korePrettyPrint/test.k
index eed64262310..59eb3f06d57 100644
--- a/k-distribution/tests/regression-new/issue-1682-korePrettyPrint/test.k
+++ b/k-distribution/tests/regression-new/issue-1682-korePrettyPrint/test.k
@@ -4,5 +4,5 @@ module TEST
syntax X ::= "a"
configuration $PGM:X
rule a => ?_:Int
- syntax Bool ::= pred1 ( Int ) [function, total, klabel(pred1), symbol, no-evaluators]
+ syntax Bool ::= pred1 ( Int ) [function, total, symbol(pred1), no-evaluators]
endmodule
diff --git a/k-distribution/tests/regression-new/issue-1760/test.k b/k-distribution/tests/regression-new/issue-1760/test.k
index 7fc1b087108..0be7ed1a953 100644
--- a/k-distribution/tests/regression-new/issue-1760/test.k
+++ b/k-distribution/tests/regression-new/issue-1760/test.k
@@ -18,13 +18,13 @@ module TEST
// Boolean Algebra Part of KAT
syntax Kat ::= Bool
- | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), group(boolOperation), hook(KAT.not)]
- > Kat "andKat" Kat [function, total, klabel(_andKat_), symbol, left, smt-hook(and), group(boolOperation), hook(KAT.and)]
- | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)]
- | Kat "=/=Kat" Kat [function, total, klabel(_=/=Kat_), symbol, left, smt-hook(distinct), hook(KAT.ne)]
- //| Kat "impliesKat" Kat [function, total, klabel(_impliesKat_), symbol, left, smt-hook(=>), group(boolOperation), hook(KAT.implies)]
+ | "notKat" Kat [function, total, symbol(notKat_), smt-hook(not), group(boolOperation), hook(KAT.not)]
+ > Kat "andKat" Kat [function, total, symbol(_andKat_), left, smt-hook(and), group(boolOperation), hook(KAT.and)]
+ | Kat "orKat" Kat [function, total, symbol(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)]
+ | Kat "=/=Kat" Kat [function, total, symbol(_=/=Kat_), left, smt-hook(distinct), hook(KAT.ne)]
+ //| Kat "impliesKat" Kat [function, total, symbol(_impliesKat_), left, smt-hook(=>), group(boolOperation), hook(KAT.implies)]
- syntax Bool ::= Kat "==Kat" Kat [function, total, klabel(_==Kat_), symbol, left, smt-hook(=), hook(KAT.eq)]
+ syntax Bool ::= Kat "==Kat" Kat [function, total, symbol(_==Kat_), left, smt-hook(=), hook(KAT.eq)]
syntax Kat ::= freshKat(Kat) [freshGenerator, function]
@@ -66,19 +66,19 @@ module TEST
/*
syntax Kat ::= "(" Kat ")" [bracket]
> left:
- Kat "Kat*" [function, klabel(_starKat), symbol, left, smtlib(ka_star), hook(KAT.mul)]
+ Kat "Kat*" [function, symbol(_starKat), left, smtlib(ka_star), hook(KAT.mul)]
> left:
- Kat "Kat;" Kat [function, klabel(_seqKat_), symbol, left, smtlib(ka_seq), hook(KAT.seq)]
+ Kat "Kat;" Kat [function, symbol(_seqKat_), left, smtlib(ka_seq), hook(KAT.seq)]
> left:
- Kat "Kat|" Kat [function, klabel(_pllKat_), symbol, left, smtlib(ka_pll), hook(KAT.pll)]
+ Kat "Kat|" Kat [function, symbol(_pllKat_), left, smtlib(ka_pll), hook(KAT.pll)]
*/
syntax Kat ::= "(" Kat ")" [bracket]
> left:
- Kat "Kat*" [function, klabel(_starKat), symbol, left, smtlib(ka_star), hook(KAT.mul)]
- | Kat "Kat;" Kat [function, klabel(_seqKat_), symbol, left, smtlib(ka_seq), hook(KAT.seq)]
- | Kat "Kat|" Kat [function, klabel(_pllKat_), symbol, left, smtlib(ka_pll), hook(KAT.pll)]
+ Kat "Kat*" [function, symbol(_starKat), left, smtlib(ka_star), hook(KAT.mul)]
+ | Kat "Kat;" Kat [function, symbol(_seqKat_), left, smtlib(ka_seq), hook(KAT.seq)]
+ | Kat "Kat|" Kat [function, symbol(_pllKat_), left, smtlib(ka_pll), hook(KAT.pll)]
rule ONE Kat; B:Kat => B:Kat
diff --git a/k-distribution/tests/regression-new/issue-1879-kproveTrans/haskell/test.k b/k-distribution/tests/regression-new/issue-1879-kproveTrans/haskell/test.k
index 12594e4fbcb..5dcbc869e0f 100644
--- a/k-distribution/tests/regression-new/issue-1879-kproveTrans/haskell/test.k
+++ b/k-distribution/tests/regression-new/issue-1879-kproveTrans/haskell/test.k
@@ -17,7 +17,7 @@ module TEST
syntax Step ::= Int
// -------------------
- syntax FInt ::= FInt ( value: Int , one: Int ) [klabel(FInt), symbol]
+ syntax FInt ::= FInt ( value: Int , one: Int ) [symbol(FInt)]
// ---------------------------------------------------------------------
syntax FInt ::= "0FInt" "(" Int ")" [macro]
diff --git a/k-distribution/tests/regression-new/issue-2321-kprovexCrash/test.k b/k-distribution/tests/regression-new/issue-2321-kprovexCrash/test.k
index 4a1a3043d98..fa394701525 100644
--- a/k-distribution/tests/regression-new/issue-2321-kprovexCrash/test.k
+++ b/k-distribution/tests/regression-new/issue-2321-kprovexCrash/test.k
@@ -4,17 +4,17 @@ module TEST
imports INT
syntax Exp ::= Int | Bool
- | pair(Int, Int) [klabel(pair), symbol]
+ | pair(Int, Int) [symbol(pair)]
- syntax KItem ::= "#assume" Exp [klabel(assume), symbol]
+ syntax KItem ::= "#assume" Exp [symbol(assume)]
rule #assume true => .K
rule #assume false => #Bottom
- syntax KItem ::= "#assert" Exp [klabel(assert), symbol]
+ syntax KItem ::= "#assert" Exp [symbol(assert)]
| "#fail"
rule #assert true => .K
rule #assert false => #fail
// Uninterpreted functions
- syntax Int ::= i(Int, Int) [function, total, no-evaluators, smtlib(fi), klabel(i)]
+ syntax Int ::= i(Int, Int) [function, total, no-evaluators, smtlib(fi), symbol(i)]
endmodule
diff --git a/k-distribution/tests/regression-new/issue-999/kat.k b/k-distribution/tests/regression-new/issue-999/kat.k
index ad420232c57..6ec30457d33 100644
--- a/k-distribution/tests/regression-new/issue-999/kat.k
+++ b/k-distribution/tests/regression-new/issue-999/kat.k
@@ -18,13 +18,13 @@ module KAT
// Boolean Algebra Part of KAT
syntax Kat ::= Bool
- | "notKat" Kat [function, total, klabel(notKat_), symbol, smt-hook(not), group(boolOperation), hook(KAT.not)]
- > Kat "andKat" Kat [function, total, klabel(_andKat_), symbol, left, smt-hook(and), group(boolOperation), hook(KAT.and)]
- | Kat "orKat" Kat [function, total, klabel(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)]
- | Kat "=/=Kat" Kat [function, total, klabel(_=/=Kat_), symbol, left, smt-hook(distinct), hook(KAT.ne)]
- //| Kat "impliesKat" Kat [function, total, klabel(_impliesKat_), symbol, left, smt-hook(=>), group(boolOperation), hook(KAT.implies)]
+ | "notKat" Kat [function, total, symbol(notKat_), smt-hook(not), group(boolOperation), hook(KAT.not)]
+ > Kat "andKat" Kat [function, total, symbol(_andKat_), left, smt-hook(and), group(boolOperation), hook(KAT.and)]
+ | Kat "orKat" Kat [function, total, symbol(_orKat_), left, smt-hook(or), group(boolOperation), hook(KAT.or)]
+ | Kat "=/=Kat" Kat [function, total, symbol(_=/=Kat_), left, smt-hook(distinct), hook(KAT.ne)]
+ //| Kat "impliesKat" Kat [function, total, symbol(_impliesKat_), left, smt-hook(=>), group(boolOperation), hook(KAT.implies)]
- syntax Bool ::= Kat "==Kat" Kat [function, total, klabel(_==Kat_), symbol, left, smt-hook(=), hook(KAT.eq)]
+ syntax Bool ::= Kat "==Kat" Kat [function, total, symbol(_==Kat_), left, smt-hook(=), hook(KAT.eq)]
syntax Kat ::= freshKat(Kat) [freshGenerator, function]
@@ -66,19 +66,19 @@ module KAT
/*
syntax Kat ::= "(" Kat ")" [bracket]
> left:
- Kat "Kat*" [function, klabel(_starKat), symbol, left, smtlib(ka_star), hook(KAT.mul)]
+ Kat "Kat*" [function, symbol(_starKat), left, smtlib(ka_star), hook(KAT.mul)]
> left:
- Kat "Kat;" Kat [function, klabel(_seqKat_), symbol, left, smtlib(ka_seq), hook(KAT.seq)]
+ Kat "Kat;" Kat [function, symbol(_seqKat_), left, smtlib(ka_seq), hook(KAT.seq)]
> left:
- Kat "Kat|" Kat [function, klabel(_pllKat_), symbol, left, smtlib(ka_pll), hook(KAT.pll)]
+ Kat "Kat|" Kat [function, symbol(_pllKat_), left, smtlib(ka_pll), hook(KAT.pll)]
*/
syntax Kat ::= "(" Kat ")" [bracket]
> left:
- Kat "Kat*" [function, klabel(_starKat), symbol, left, smtlib(ka_star), hook(KAT.mul)]
- | Kat "Kat;" Kat [function, klabel(_seqKat_), symbol, left, smtlib(ka_seq), hook(KAT.seq)]
- | Kat "Kat|" Kat [function, klabel(_pllKat_), symbol, left, smtlib(ka_pll), hook(KAT.pll)]
+ Kat "Kat*" [function, symbol(_starKat), left, smtlib(ka_star), hook(KAT.mul)]
+ | Kat "Kat;" Kat [function, symbol(_seqKat_), left, smtlib(ka_seq), hook(KAT.seq)]
+ | Kat "Kat|" Kat [function, symbol(_pllKat_), left, smtlib(ka_pll), hook(KAT.pll)]
rule ONE Kat; B:Kat => B:Kat
diff --git a/k-distribution/tests/regression-new/pl-tutorial/2_languages/2_kool/2_typed/2_static/kool-typed-static.md b/k-distribution/tests/regression-new/pl-tutorial/2_languages/2_kool/2_typed/2_static/kool-typed-static.md
index 0669f2b0629..bba11c2331d 100644
--- a/k-distribution/tests/regression-new/pl-tutorial/2_languages/2_kool/2_typed/2_static/kool-typed-static.md
+++ b/k-distribution/tests/regression-new/pl-tutorial/2_languages/2_kool/2_typed/2_static/kool-typed-static.md
@@ -125,7 +125,7 @@ the wrapper in the generated documentation, we associate it an
```k
syntax Type ::= "void" | "int" | "bool" | "string"
- | Id [klabel("class"), symbol, avoid] // see next
+ | Id [symbol("class"), avoid] // see next
| Type "[" "]"
| "(" Type ")" [bracket]
> Types "->" Type
diff --git a/k-distribution/tests/regression-new/pl-tutorial/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md b/k-distribution/tests/regression-new/pl-tutorial/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md
index db442366b66..80e6182dafd 100644
--- a/k-distribution/tests/regression-new/pl-tutorial/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md
+++ b/k-distribution/tests/regression-new/pl-tutorial/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md
@@ -350,7 +350,7 @@ a constructor for function types:
| "(" Type ")" [bracket]
| TypeVar
| TypeName [klabel(TypeName), avoid]
- | Type TypeName [klabel(Type-TypeName), symbol, macro]
+ | Type TypeName [symbol(Type-TypeName), macro]
| "(" Types ")" TypeName [prefer]
syntax Types ::= List{Type,","} [klabel(types)]
syntax Types ::= TypeVars
diff --git a/k-distribution/tests/regression-new/unparseKORE/test.k b/k-distribution/tests/regression-new/unparseKORE/test.k
index f57646f8187..51fed8939bf 100644
--- a/k-distribution/tests/regression-new/unparseKORE/test.k
+++ b/k-distribution/tests/regression-new/unparseKORE/test.k
@@ -5,8 +5,8 @@ module TEST
syntax A ::= "a1" A
| "a2" A
- | "a1" [klabel(b1), symbol]
- | "a2" [klabel(a2), symbol]
+ | "a1" [symbol(b1)]
+ | "a2" [symbol(a2)]
rule a1 => #unparseKORE(a1)
rule a2 => #unparseKORE(a2)