1 files changed, 9 insertions, 0 deletions
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 271c8bc7a..2b1901f5d 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -239,6 +239,15 @@ function constant {
   register_kind "$1" 0 "$5"
 }
 
+function nullaryoperator {
+  # nullaryoperator K ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  check_theory_seen
+  register_kind "$1" 0 "$2"
+}
+
 function register_sort {
   id=$1
   cardinality=$2