diff --git a/src/cmd_parser.cpp b/src/cmd_parser.cpp
index ab37650f..d7faa839 100644
--- a/src/cmd_parser.cpp
+++ b/src/cmd_parser.cpp
@@ -33,9 +33,6 @@ CmdParser::CmdParser(Lexer& lex,
   d_table["declare-const"] = Token::DECLARE_CONST;
   d_table["declare-datatype"] = Token::DECLARE_DATATYPE;
   d_table["declare-datatypes"] = Token::DECLARE_DATATYPES;
-  d_table["declare-fun"] = Token::DECLARE_FUN;
-  d_table["declare-sort"] = Token::DECLARE_SORT;
-  d_table["define-const"] = Token::DEFINE_CONST;
   d_table["echo"] = Token::ECHO;
   d_table["exit"] = Token::EXIT;
   d_table["pop"] = Token::POP;
@@ -54,6 +51,9 @@ CmdParser::CmdParser(Lexer& lex,
   {
     // only used in smt2 queries
     d_table["assert"] = Token::ASSERT;
+    d_table["declare-fun"] = Token::DECLARE_FUN;
+    d_table["declare-sort"] = Token::DECLARE_SORT;
+    d_table["define-const"] = Token::DEFINE_CONST;
     d_table["define-fun"] = Token::DEFINE_FUN;
     d_table["define-sort"] = Token::DEFINE_SORT;
     d_table["check-sat"] = Token::CHECK_SAT;
@@ -173,7 +173,7 @@ bool CmdParser::parseNextCommand()
         cons = d_state.mkLiteral(Kind::STRING, oname);
         // don't permit attributes for oracle functions
       }
-      else if (tok==Token::DECLARE_CONST || tok==Token::DECLARE_FUN || tok==Token::DECLARE_PARAMETERIZED_CONST)
+      else if (tok==Token::DECLARE_CONST || tok==Token::DECLARE_PARAMETERIZED_CONST)
       {
         // possible attribute list
         AttrMap attrs;
@@ -181,6 +181,7 @@ bool CmdParser::parseNextCommand()
         // determine if an attribute specified a constructor kind
         d_eparser.processAttributeMap(attrs, ck, cons, params);
       }
+      // declare-fun does not parse attribute list, as it is only in smt2
       t = ret;
       if (!sorts.empty())
       {
diff --git a/tests/Arith-theory.smt3 b/tests/Arith-theory.smt3
index 09c1d93c..2912324d 100644
--- a/tests/Arith-theory.smt3
+++ b/tests/Arith-theory.smt3
@@ -1,7 +1,7 @@
 (include "Builtin-theory.smt3")
 
-(declare-sort Int 0)
-(declare-sort Real 0)
+(declare-type Int ())
+(declare-type Real ())
 
 (declare-consts <numeral> Int)
 (declare-consts <rational> Real)
diff --git a/tests/Sets-theory.smt3 b/tests/Sets-theory.smt3
index b13e4bad..ebb38747 100644
--- a/tests/Sets-theory.smt3
+++ b/tests/Sets-theory.smt3
@@ -2,7 +2,7 @@
 (include "Arith-theory.smt3")
 (include "Datatypes-theory.smt3")
 
-(declare-sort Set 1)
+(declare-type Set (Type))
 
 ; NOTE: permits non-set types
 (declare-const set.empty (-> (! Type :var T) T))
diff --git a/tests/Strings-theory.smt3 b/tests/Strings-theory.smt3
index 0beedb51..b196c362 100644
--- a/tests/Strings-theory.smt3
+++ b/tests/Strings-theory.smt3
@@ -1,9 +1,9 @@
 (include "Builtin-theory.smt3")
 (include "Arith-theory.smt3")
 
-(declare-sort RegLan 0)
+(declare-type RegLan ())
 (declare-type Seq (Type))
-(declare-sort Char 0)
+(declare-type Char ())
 (define String () (Seq Char))
 
 (declare-consts <string> String)
diff --git a/tests/Utils.smt3 b/tests/Utils.smt3
index 7848c3e3..2a2eb8e8 100644
--- a/tests/Utils.smt3
+++ b/tests/Utils.smt3
@@ -26,7 +26,7 @@
 )
 
 ; untyped list
-(declare-sort @List 0)
+(declare-type @List ())
 (declare-const @list.nil @List)
 (declare-const @list (-> (! Type :var T :implicit) T @List @List) :right-assoc-nil @list.nil)
 
diff --git a/tests/arith-eval.smt3 b/tests/arith-eval.smt3
index 9f86a7c8..61c15ecd 100644
--- a/tests/arith-eval.smt3
+++ b/tests/arith-eval.smt3
@@ -1,5 +1,5 @@
-(declare-sort Int 0)
-(declare-sort Real 0)
+(declare-type Int ())
+(declare-type Real ())
 
 (declare-consts <numeral> Int)
 (declare-consts <rational> Real)
diff --git a/tests/arith-rules-test.smt3 b/tests/arith-rules-test.smt3
index 99a29b7e..2ba86921 100644
--- a/tests/arith-rules-test.smt3
+++ b/tests/arith-rules-test.smt3
@@ -1,9 +1,9 @@
 (include "Arith-rules.smt3")
 
-(declare-fun x () Int)
-(declare-fun y () Int)
-(declare-fun z () Int)
-(declare-fun w () Int)
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(declare-const w Int)
 
 (assume @p0 (< x (* 2 y)))
 (assume @p1 (< y z))
diff --git a/tests/arity-overload.smt3 b/tests/arity-overload.smt3
index 14837a77..d6167bcd 100644
--- a/tests/arity-overload.smt3
+++ b/tests/arity-overload.smt3
@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const - (-> Int Int))
 (declare-const - (-> Int Int Int))
 
diff --git a/tests/beta-reduce-define-fun.smt3 b/tests/beta-reduce-define-fun.smt3
index 3d1ddcdd..73cb724d 100644
--- a/tests/beta-reduce-define-fun.smt3
+++ b/tests/beta-reduce-define-fun.smt3
@@ -4,7 +4,7 @@
 (declare-const not (-> Bool Bool))
 
 
-(declare-sort U 0)
+(declare-type U ())
 (define f_true ((x U)) true)
 
 
diff --git a/tests/binder-ex.smt3 b/tests/binder-ex.smt3
index 684ede18..faa79c31 100644
--- a/tests/binder-ex.smt3
+++ b/tests/binder-ex.smt3
@@ -1,8 +1,8 @@
-(declare-sort @List 0)
+(declare-type @List ())
 (declare-const @list.nil @List)
 (declare-const @list.cons (-> (! Type :var T :implicit) T @List @List) :right-assoc-nil @list.nil)
 
-(declare-sort Int 0)
+(declare-type Int ())
 
 (declare-const P (-> Int Bool))
 (declare-const forall (-> @List Bool Bool) :binder @list.cons)
diff --git a/tests/binder-subterm-share.smt3 b/tests/binder-subterm-share.smt3
index 37f429e5..981f7912 100644
--- a/tests/binder-subterm-share.smt3
+++ b/tests/binder-subterm-share.smt3
@@ -1,8 +1,8 @@
-(declare-sort @List 0)
+(declare-type @List ())
 (declare-const @list.nil @List)
 (declare-const @list.cons (-> (! Type :var T :implicit) T @List @List) :right-assoc-nil @list.nil)
 
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const P (-> Int Bool))
 (declare-const forall (-> @List Bool Bool) :binder @list.cons)
 (declare-rule id ((y Bool)) :premises (y) :conclusion y)
diff --git a/tests/bv-concat.smt3 b/tests/bv-concat.smt3
index 1b4e2a81..1f08833d 100644
--- a/tests/bv-concat.smt3
+++ b/tests/bv-concat.smt3
@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 
 (declare-type BitVec (Int)) 
@@ -18,7 +18,7 @@
   (BitVec (alf.add n m))))
   
 
-(declare-fun x () (BitVec 2))
-(declare-fun y () (BitVec 3))
+(declare-const x (BitVec 2))
+(declare-const y (BitVec 3))
 (define z () (bvconcat x y) :type (BitVec 5))
 
diff --git a/tests/bv-dep-type.smt3 b/tests/bv-dep-type.smt3
index 53bd0708..5837d5a8 100644
--- a/tests/bv-dep-type.smt3
+++ b/tests/bv-dep-type.smt3
@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 
 (declare-type BitVec (Int)) 
 
@@ -8,9 +8,9 @@
   (BitVec n)
   (BitVec n)))
 
-(declare-fun m () Int)
-(declare-fun dummy () Int)
+(declare-const m Int)
+(declare-const dummy Int)
 
-(declare-fun x () (BitVec m))
-(declare-fun y () (BitVec m))
+(declare-const x (BitVec m))
+(declare-const y (BitVec m))
 (define z () (bvadd m x y) :type (BitVec m))
diff --git a/tests/bv-eval.smt3 b/tests/bv-eval.smt3
index 245dec23..85f0faa2 100644
--- a/tests/bv-eval.smt3
+++ b/tests/bv-eval.smt3
@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 
 (declare-const = (-> (! Type :var T :implicit) T T Bool))
diff --git a/tests/bv-extract-smt3.smt3 b/tests/bv-extract-smt3.smt3
index f29909db..2c8e80de 100644
--- a/tests/bv-extract-smt3.smt3
+++ b/tests/bv-extract-smt3.smt3
@@ -1,7 +1,7 @@
 (declare-const = (-> (! Type :var A :implicit) A A Bool))
 
 (declare-const and (-> Bool Bool Bool) :left-assoc)
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const < (-> Int Int Bool))
 (declare-const <= (-> Int Int Bool) :chainable and)
 (declare-const - (-> Int Int Int))
diff --git a/tests/bv-extract.smt3 b/tests/bv-extract.smt3
index 34e4092e..17fc85a4 100644
--- a/tests/bv-extract.smt3
+++ b/tests/bv-extract.smt3
@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 (declare-const BitVec (-> Int Type))
 
diff --git a/tests/bv-literals.smt3 b/tests/bv-literals.smt3
index 879bb859..b8004fa7 100644
--- a/tests/bv-literals.smt3
+++ b/tests/bv-literals.smt3
@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 
 (declare-const = (-> (! Type :var T :implicit) T T Bool))
diff --git a/tests/bv-type-strict.smt3 b/tests/bv-type-strict.smt3
index 3ba2beb3..609e39e7 100644
--- a/tests/bv-type-strict.smt3
+++ b/tests/bv-type-strict.smt3
@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 
 (declare-const = (-> (! Type :var T :implicit) T T Bool))
diff --git a/tests/constant-eval-args.smt3 b/tests/constant-eval-args.smt3
index 9cadfaca..7724c405 100644
--- a/tests/constant-eval-args.smt3
+++ b/tests/constant-eval-args.smt3
@@ -1,5 +1,5 @@
 
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 
 (program less-than ()
diff --git a/tests/constant-eval.smt3 b/tests/constant-eval.smt3
index c3027c7d..2263b4d9 100644
--- a/tests/constant-eval.smt3
+++ b/tests/constant-eval.smt3
@@ -1,6 +1,6 @@
 
 
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 
 (program less-than ()
diff --git a/tests/datatype-simple.smt3 b/tests/datatype-simple.smt3
index 7d2eb549..762b32fd 100644
--- a/tests/datatype-simple.smt3
+++ b/tests/datatype-simple.smt3
@@ -3,7 +3,7 @@
 
 (declare-datatypes ((nat 0)(list 0)(tree 0))
   (((succ (pred nat)) (zero))((cons (car tree) (cdr list)) (null))((node (data nat) (children list)) (leaf))))
-(declare-fun x () nat)
-(declare-fun y () list)
-(declare-fun z () tree)
+(declare-const x nat)
+(declare-const y list)
+(declare-const z tree)
 (assume a1 (= x (succ zero)))
diff --git a/tests/define-const-simple.smt3 b/tests/define-const-simple.smt3
index 86fd6cee..c527fd1c 100644
--- a/tests/define-const-simple.smt3
+++ b/tests/define-const-simple.smt3
@@ -1,7 +1,7 @@
 
 (declare-const not (-> Bool Bool))
 
-(define-const f_true Bool true)
+(define f_true () true)
 
 
 (declare-rule trust ((f Bool))
diff --git a/tests/define-sort-iarray.smt3 b/tests/define-sort-iarray.smt3
index 0eb698ee..e59403c0 100644
--- a/tests/define-sort-iarray.smt3
+++ b/tests/define-sort-iarray.smt3
@@ -1,7 +1,7 @@
 
 (declare-const = (-> (! Type :var T :implicit) T T Bool))
-(declare-sort Array 2)
-(declare-sort Int 0)
+(declare-type Array (Type Type))
+(declare-type Int ())
 (define IntArray ((T Type)) (Array Int T))
 (declare-const a (Array Int Bool))
 (declare-const b (IntArray Bool))
diff --git a/tests/distinct_value_testers.smt3 b/tests/distinct_value_testers.smt3
index 9ba4d2ec..b5398d2b 100644
--- a/tests/distinct_value_testers.smt3
+++ b/tests/distinct_value_testers.smt3
@@ -7,7 +7,7 @@
     :conclusion (not (= t s))
 )
 
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 
 (declare-rule disinct_value_int ((t Int) (s Int))
@@ -16,7 +16,7 @@
     :conclusion (not (= t s))
 )
 
-(declare-sort Real 0)
+(declare-type Real ())
 (declare-consts <rational> Real)
 
 (declare-rule disinct_value_real ((t Real) (s Real))
@@ -26,7 +26,7 @@
 )
 
 
-(declare-sort String 0)
+(declare-type String ())
 (declare-consts <string> String)
 
 (declare-rule disinct_value_str ((t String) (s String))
@@ -35,7 +35,7 @@
     :conclusion (not (= t s))
 )
 
-(declare-sort Bin 0)
+(declare-type Bin ())
 (declare-consts <binary> Bin)
 
 (declare-rule disinct_value_bin ((t Bin) (s Bin))
diff --git a/tests/eval-inc.smt3 b/tests/eval-inc.smt3
index f1e0141f..cbe17b4a 100644
--- a/tests/eval-inc.smt3
+++ b/tests/eval-inc.smt3
@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 
 (declare-consts <numeral> Int)
 
diff --git a/tests/evaluate.smt3 b/tests/evaluate.smt3
index ee01dbcc..87f31be3 100644
--- a/tests/evaluate.smt3
+++ b/tests/evaluate.smt3
@@ -1,5 +1,5 @@
 
-(declare-sort Int 0)
+(declare-type Int ())
 
 (declare-const and (-> Bool Bool Bool))
 (declare-const i0 Int)
@@ -21,7 +21,7 @@
 )
 
 
-(declare-fun P () Bool)
-(declare-fun Q () Bool)
+(declare-const P Bool)
+(declare-const Q Bool)
 (assume a0 (and P Q))
 (step a1 P :rule and_elim :premises (a0) :args (i0))
diff --git a/tests/evaluation.smt3 b/tests/evaluation.smt3
index 696bbc92..d15b7279 100644
--- a/tests/evaluation.smt3
+++ b/tests/evaluation.smt3
@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 
 (declare-consts <numeral> Int)
 
diff --git a/tests/ff-nil.smt3 b/tests/ff-nil.smt3
index 759903d6..06f7bc17 100644
--- a/tests/ff-nil.smt3
+++ b/tests/ff-nil.smt3
@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 (declare-const FiniteField (-> Int Type))
 
@@ -10,7 +10,7 @@
     :right-assoc-nil (ff.value p 0)
 )
 
-(declare-fun c () (_ FiniteField 17))
+(declare-const c (_ FiniteField 17))
 
 (declare-const eq (-> (! Type :var T :implicit) T T Bool))
 
diff --git a/tests/generic-swap.smt3 b/tests/generic-swap.smt3
index b10f06c8..1f2bb521 100644
--- a/tests/generic-swap.smt3
+++ b/tests/generic-swap.smt3
@@ -1,4 +1,4 @@
-(declare-sort Pair 1)
+(declare-type Pair (Type))
 
 (declare-const pair (-> (! Type :var T :implicit) T T (Pair T)))
 
@@ -19,7 +19,7 @@
   :conclusion (is_swap t (swap t))
 )
 
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const a Int)
 (declare-const b Int)
 
diff --git a/tests/gt_eval.smt3 b/tests/gt_eval.smt3
index f6a4643c..623148c2 100644
--- a/tests/gt_eval.smt3
+++ b/tests/gt_eval.smt3
@@ -1,5 +1,5 @@
 
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 (declare-const > (-> Int Int Bool))
 
@@ -9,7 +9,7 @@
     :conclusion (> t s)
 )
 
-(declare-sort Bin 0)
+(declare-type Bin ())
 (declare-consts <binary> Bin)
 (declare-const bvugt (-> Bin Bin Bool))
 
diff --git a/tests/ite-compile-test.smt3 b/tests/ite-compile-test.smt3
index aa8692ca..edba9525 100644
--- a/tests/ite-compile-test.smt3
+++ b/tests/ite-compile-test.smt3
@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 (declare-const + (-> Int Int Int))
 (declare-const - (-> Int Int Int))
@@ -25,7 +25,7 @@
   )
 )
 
-(declare-fun f (Int) Int)
+(declare-const f (-> Int Int))
 
 
 (declare-rule eval_factorial ((x Int))
@@ -35,7 +35,7 @@
 (step @p0 (= (f 4) 24) :rule eval_factorial :args (4))
 
 
-(declare-fun e (Int) Int)
+(declare-const e (-> Int Int))
 
 (declare-rule eval_check_sign ((x Int))
   :args (x)
diff --git a/tests/literals.smt3 b/tests/literals.smt3
index 39ded750..46df88a5 100644
--- a/tests/literals.smt3
+++ b/tests/literals.smt3
@@ -1,6 +1,6 @@
 
 
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 
 (declare-const and (-> Bool Bool Bool))
@@ -29,8 +29,8 @@
    :conclusion (select i (and f g))
 )
 
-(declare-fun P () Bool)
-(declare-fun Q () Bool)
+(declare-const P Bool)
+(declare-const Q Bool)
 (assume a0 (and P Q))
 (step a1 Q :rule and_elim :premises (a0) :args (1))
 
diff --git a/tests/match-simple.smt3 b/tests/match-simple.smt3
index 49124005..6c9ae0ab 100644
--- a/tests/match-simple.smt3
+++ b/tests/match-simple.smt3
@@ -1,7 +1,7 @@
 
 (declare-const => (-> Bool Bool Bool))
 
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 
 (declare-type Pair (Type Type))
diff --git a/tests/match-variants.smt3 b/tests/match-variants.smt3
index f2c2e0e5..59d546ba 100644
--- a/tests/match-variants.smt3
+++ b/tests/match-variants.smt3
@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const a Int)
 (declare-const b Int)
 (declare-const P (-> Int Bool))
diff --git a/tests/mixed-arith.smt3 b/tests/mixed-arith.smt3
index 4c26f359..d09f0518 100644
--- a/tests/mixed-arith.smt3
+++ b/tests/mixed-arith.smt3
@@ -1,5 +1,5 @@
-(declare-sort Int 0)
-(declare-sort Real 0)
+(declare-type Int ())
+(declare-type Real ())
 
 (declare-consts <numeral> Int)
 (declare-consts <rational> Real)
diff --git a/tests/mutual-rec.smt3 b/tests/mutual-rec.smt3
index 187512a9..42230df9 100644
--- a/tests/mutual-rec.smt3
+++ b/tests/mutual-rec.smt3
@@ -1,6 +1,6 @@
 
 
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 
 ; forward declaration
@@ -24,8 +24,8 @@
   )
 )
 
-(declare-fun not (Bool) Bool)
-(declare-fun pred_is_even (Int) Bool)
+(declare-const not (-> Bool Bool))
+(declare-const pred_is_even (-> Int Bool))
 
 (declare-rule find_is_even ((n Int))
    :args (n)
diff --git a/tests/nat-type.smt3 b/tests/nat-type.smt3
index 742175d3..e7759d68 100644
--- a/tests/nat-type.smt3
+++ b/tests/nat-type.smt3
@@ -1,8 +1,8 @@
-(declare-sort Nat 0)
+(declare-type Nat ())
 
 (declare-consts <numeral> (! Nat :requires ((alf.is_neg alf.self) false)))
 
-(declare-fun f (Nat) Bool)
+(declare-const f (-> Nat Bool))
 
 (assume @p0 (f 0))
 ;(assume @p0 (f (alf.neg 1)))
diff --git a/tests/nground-nil-v3.smt3 b/tests/nground-nil-v3.smt3
index 9a72cff5..214fff1e 100644
--- a/tests/nground-nil-v3.smt3
+++ b/tests/nground-nil-v3.smt3
@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 
 (declare-const BitVec (-> Int Type))
diff --git a/tests/opaque-inst.smt3 b/tests/opaque-inst.smt3
index 3d77d216..1a5b0d72 100644
--- a/tests/opaque-inst.smt3
+++ b/tests/opaque-inst.smt3
@@ -7,8 +7,8 @@
 (declare-const and (-> Bool Bool Bool) :right-assoc-nil true)
 (declare-const not (-> Bool Bool))
 
-(declare-sort Array 2)
-(declare-sort Int 0)
+(declare-type Array (Type Type))
+(declare-type Int ())
 
 (declare-const select (-> (Array Int Int) Int Int))
 
diff --git a/tests/opaque-inst2.smt3 b/tests/opaque-inst2.smt3
index f84c2797..9181f381 100644
--- a/tests/opaque-inst2.smt3
+++ b/tests/opaque-inst2.smt3
@@ -7,8 +7,8 @@
 (declare-const and (-> Bool Bool Bool) :right-assoc-nil true)
 (declare-const not (-> Bool Bool))
 
-(declare-sort Array 2)
-(declare-sort Int 0)
+(declare-type Array (Type Type))
+(declare-type Int ())
 
 (declare-const select (-> (Array Int Int) Int Int))
 
diff --git a/tests/oracle-ex.smt3 b/tests/oracle-ex.smt3
index 1417c4a3..f4db66f3 100644
--- a/tests/oracle-ex.smt3
+++ b/tests/oracle-ex.smt3
@@ -1,6 +1,6 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
-(declare-sort String 0)
+(declare-type String ())
 (declare-consts <string> String)
 (declare-const or (-> Bool Bool Bool) :right-assoc-nil false)
 (declare-const and (-> Bool Bool Bool) :right-assoc-nil true)
diff --git a/tests/oracle-ex2.smt3 b/tests/oracle-ex2.smt3
index e4992dcd..98860d45 100644
--- a/tests/oracle-ex2.smt3
+++ b/tests/oracle-ex2.smt3
@@ -1,6 +1,6 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
-(declare-sort String 0)
+(declare-type String ())
 (declare-consts <string> String)
 (declare-const or (-> Bool Bool Bool) :right-assoc-nil false)
 (declare-const and (-> Bool Bool Bool) :right-assoc-nil true)
diff --git a/tests/overloading-as.smt3 b/tests/overloading-as.smt3
index 3ef1b075..0efdc1f3 100644
--- a/tests/overloading-as.smt3
+++ b/tests/overloading-as.smt3
@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const - (-> Int Int Int))
 (declare-const - (-> Int Int))
 
diff --git a/tests/overloading.smt3 b/tests/overloading.smt3
index dd6a0d85..2a0e1bb3 100644
--- a/tests/overloading.smt3
+++ b/tests/overloading.smt3
@@ -1,5 +1,5 @@
-(declare-sort Int 0)
-(declare-sort Real 0)
+(declare-type Int ())
+(declare-type Real ())
 
 (program a.typeunion ()
     (Type Type) Type
diff --git a/tests/pairwise.smt3 b/tests/pairwise.smt3
index 5d4d8d5f..d919ed00 100644
--- a/tests/pairwise.smt3
+++ b/tests/pairwise.smt3
@@ -11,7 +11,7 @@
    :conclusion a
 )
 
-(declare-sort U 0)
+(declare-type U ())
 
 (declare-const a U)
 (declare-const b U)
diff --git a/tests/par-dt.smt3 b/tests/par-dt.smt3
index 6c3b5b51..dbcbd803 100644
--- a/tests/par-dt.smt3
+++ b/tests/par-dt.smt3
@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-datatypes ((List 1)) ((par (T) ((nil) (cons (head T) (tail (List T)))))))
 (define y () (alf.var "y" (List Int)))
 (define @t1 () (tail y) :type (List Int))
diff --git a/tests/pf-haniel.smt3 b/tests/pf-haniel.smt3
index 51fa5602..d51f7c05 100644
--- a/tests/pf-haniel.smt3
+++ b/tests/pf-haniel.smt3
@@ -1,15 +1,15 @@
 (include "Uf-rules.smt3")
 (include "Builtin-rules.smt3")
 (include "Booleans-rules.smt3")
-(declare-sort U 0)
-(declare-fun f (U U) U)
-(declare-fun p2 () Bool)
-(declare-fun p3 () Bool)
-(declare-fun p1 () Bool)
-(declare-fun c () U)
-(declare-fun d () U)
-(declare-fun a () U)
-(declare-fun b () U)
+(declare-type U ())
+(declare-const f (-> U U U))
+(declare-const p2 Bool)
+(declare-const p3 Bool)
+(declare-const p1 Bool)
+(declare-const c U)
+(declare-const d U)
+(declare-const a U)
+(declare-const b U)
 (define @t1 () (= a b))
 (define @t2 () (= c d))
 (define @t3 () (and p1 true))
diff --git a/tests/pf-quant.smt3 b/tests/pf-quant.smt3
index c198f2a3..3fb56e1f 100644
--- a/tests/pf-quant.smt3
+++ b/tests/pf-quant.smt3
@@ -1,6 +1,6 @@
 (include "./quant.smt3")
 
-(declare-sort Int 0)
+(declare-type Int ())
 
 (define x1 () (alf.var "x1" Int))
 (declare-const a Int)
diff --git a/tests/pf-simple-sig-2.smt3 b/tests/pf-simple-sig-2.smt3
index 0c32afcd..f525ec63 100644
--- a/tests/pf-simple-sig-2.smt3
+++ b/tests/pf-simple-sig-2.smt3
@@ -1,8 +1,8 @@
 
 (include "./simple-sig-2.smt3")
 
-(declare-sort Int 0)
-(declare-fun a () Int)
-(declare-fun b () Int)
+(declare-type Int ())
+(declare-const a Int)
+(declare-const b Int)
 (assume a1 (= a b))
 (step a2 (= b a) :rule eq-symm-flip :premises (a1))
diff --git a/tests/pf-simple-sig.smt3 b/tests/pf-simple-sig.smt3
index 2409d3a4..aa3d48a6 100644
--- a/tests/pf-simple-sig.smt3
+++ b/tests/pf-simple-sig.smt3
@@ -1,10 +1,10 @@
 
 (include "./simple-sig.smt3")
 
-(declare-sort Int 0)
-(declare-fun a () Int)
-(declare-fun b () Int)
-(declare-fun c () Bool)
+(declare-type Int ())
+(declare-const a Int)
+(declare-const b Int)
+(declare-const c Bool)
 (assume a1 (= a b))
 (assume a2 (not (= b a)))
 (step a3 (= b a) :rule eq-symm :premises (a1) :args ())
diff --git a/tests/premise-list-cong-2.smt3 b/tests/premise-list-cong-2.smt3
index f58c1e26..290dd01c 100644
--- a/tests/premise-list-cong-2.smt3
+++ b/tests/premise-list-cong-2.smt3
@@ -24,12 +24,12 @@
 )
 
 
-(declare-sort U 0)
+(declare-type U ())
 (declare-const a U)
 (declare-const b U)
 (declare-const c U)
 (declare-const d U)
-(declare-fun f (U U) U)
+(declare-const f (-> U U U))
 
 (assume @p0 (= a b))
 (assume @p1 (= c d))
diff --git a/tests/premise-list-cong.smt3 b/tests/premise-list-cong.smt3
index cd489c08..2b0ccf9b 100644
--- a/tests/premise-list-cong.smt3
+++ b/tests/premise-list-cong.smt3
@@ -16,12 +16,12 @@
     :conclusion (mk_cong_eq (= f f) E)
 )
 
-(declare-sort U 0)
+(declare-type U ())
 (declare-const a U)
 (declare-const b U)
 (declare-const c U)
 (declare-const d U)
-(declare-fun f (U U) U)
+(declare-const f (-> U U U))
 
 (assume @p0 (= a b))
 (assume @p1 (= c d))
diff --git a/tests/push-pop.smt3 b/tests/push-pop.smt3
index 76ee0717..3124599a 100644
--- a/tests/push-pop.smt3
+++ b/tests/push-pop.smt3
@@ -7,7 +7,7 @@
     :conclusion (= t t)
 )
 
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const b Int)
 
 (push)
diff --git a/tests/quant-sk-small.alfc.smt3 b/tests/quant-sk-small.alfc.smt3
index 5d9860ea..792d430c 100644
--- a/tests/quant-sk-small.alfc.smt3
+++ b/tests/quant-sk-small.alfc.smt3
@@ -5,7 +5,7 @@
 (define alf.1.x () (alf.var "alf.1.x" Int))
 (define x () (alf.var "x" Int))
 (define y () (alf.var "y" Int))
-(declare-fun P (Int Int) Bool)
+(declare-const P (-> Int Int Bool))
 (define @t1 () (forall (@list x y) (P x y)))
 (define @t2 () (P alf.1.x 5))
 (define @t3 () (exists (@list alf.1.x @list.nil) (not @t2)))
diff --git a/tests/quoted.smt3 b/tests/quoted.smt3
index 28c1c205..2f717946 100644
--- a/tests/quoted.smt3
+++ b/tests/quoted.smt3
@@ -11,10 +11,10 @@
   :conclusion (= Bool (= T x y) (= T y x)))
   
 
-(declare-sort Int 0)
-(declare-fun x () Int)
-(declare-fun y () Int)
-(declare-fun c () Bool)
+(declare-type Int ())
+(declare-const x Int)
+(declare-const y Int)
+(declare-const c Bool)
 (step a5 (= Bool (= Int x y) (= Int y x)) :rule eq-symm-taut :premises () :args ((= Int x y)))
 ;(step a6 (= Bool (= Int x y) (= Int y x)) :rule eq-symm-taut :premises () :args (x))
 
diff --git a/tests/requires.smt3 b/tests/requires.smt3
index fcf3d5bd..8f21b487 100644
--- a/tests/requires.smt3
+++ b/tests/requires.smt3
@@ -1,5 +1,5 @@
 
-(declare-sort Int 0)
+(declare-type Int ())
 
 (declare-const and (-> Bool Bool Bool))
 (declare-const i0 Int)
@@ -22,8 +22,8 @@
 )
 
 
-(declare-fun P () Bool)
-(declare-fun Q () Bool)
+(declare-const P Bool)
+(declare-const Q Bool)
 (assume a0 (and P Q))
 (step a1 P :rule and_elim :premises (a0) :args (i0))
 
diff --git a/tests/right-assoc-variants.smt3 b/tests/right-assoc-variants.smt3
index 12291482..3ae9ab2c 100644
--- a/tests/right-assoc-variants.smt3
+++ b/tests/right-assoc-variants.smt3
@@ -1,8 +1,8 @@
 
-(declare-sort Int 0)
-(declare-sort Real 0)
+(declare-type Int ())
+(declare-type Real ())
 (declare-const BitVec (-> Int Type))
-(declare-sort String 0)
+(declare-type String ())
 (declare-type Seq (Type))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/tests/self-requires.smt3 b/tests/self-requires.smt3
index 428a883c..58a7395b 100644
--- a/tests/self-requires.smt3
+++ b/tests/self-requires.smt3
@@ -1,3 +1,3 @@
-(declare-sort Nat 0)
+(declare-type Nat ())
 
 (declare-consts <numeral> (! Nat :requires ((alf.is_neg alf.self) false)))
diff --git a/tests/simple-pf-implicit.smt3 b/tests/simple-pf-implicit.smt3
index 810437ec..426371f4 100644
--- a/tests/simple-pf-implicit.smt3
+++ b/tests/simple-pf-implicit.smt3
@@ -8,9 +8,9 @@
   :conclusion (= y x))
 
   
-(declare-sort Int 0)
-(declare-fun a () Int)
-(declare-fun b () Int)
-(declare-fun c () Bool)
+(declare-type Int ())
+(declare-const a Int)
+(declare-const b Int)
+(declare-const c Bool)
 (assume a1 (= a b))
 (step a2 (= b a) :rule eq-symm :premises (a1) :args ())
diff --git a/tests/simple-pf.smt3 b/tests/simple-pf.smt3
index af0a9338..4ae418a6 100644
--- a/tests/simple-pf.smt3
+++ b/tests/simple-pf.smt3
@@ -8,10 +8,10 @@
   :conclusion (= T y x))
 
   
-(declare-sort Int 0)
-(declare-fun a () Int)
-(declare-fun b () Int)
-(declare-fun c () Bool)
+(declare-type Int ())
+(declare-const a Int)
+(declare-const b Int)
+(declare-const c Bool)
 (assume a1 (= Int a b))
 (step a2 (= Int b a) :rule eq-symm :premises (a1) :args ())
 
diff --git a/tests/simple-pf2.smt3 b/tests/simple-pf2.smt3
index 92edbedf..7fbe6619 100644
--- a/tests/simple-pf2.smt3
+++ b/tests/simple-pf2.smt3
@@ -14,10 +14,10 @@
   :conclusion false
 )
 
-(declare-sort Int 0)
-(declare-fun x () Int)
-(declare-fun y () Int)
-(declare-fun c () Bool)
+(declare-type Int ())
+(declare-const x Int)
+(declare-const y Int)
+(declare-const c Bool)
 (assume a1 (= Int x y))
 (assume a2 (not (= Int y x)))
 (step a3 (= Int y x) :rule eq-symm :premises (a1) :args ())
diff --git a/tests/simple-program.smt3 b/tests/simple-program.smt3
index 73f00d1b..5af795e8 100644
--- a/tests/simple-program.smt3
+++ b/tests/simple-program.smt3
@@ -1,5 +1,5 @@
 
-(declare-sort Int 0)
+(declare-type Int ())
 
 (declare-const and (-> Bool Bool Bool))
 (declare-const i0 Int)
diff --git a/tests/simple.smt3 b/tests/simple.smt3
index 2c35f61a..6734c8b4 100644
--- a/tests/simple.smt3
+++ b/tests/simple.smt3
@@ -1,3 +1,3 @@
-(declare-sort Int 0)
-(declare-fun x () Int)
+(declare-type Int ())
+(declare-const x Int)
 (define y () x :type Int)
diff --git a/tests/str-eval.smt3 b/tests/str-eval.smt3
index bd964b9c..4bad17b4 100644
--- a/tests/str-eval.smt3
+++ b/tests/str-eval.smt3
@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 
 (declare-const = (-> (! Type :var T :implicit) T T Bool))
@@ -15,7 +15,7 @@
     )
 )
 
-(declare-sort String 0)
+(declare-type String ())
 (declare-consts <string> String)
   
 (declare-const str.++ (-> String String String))
diff --git a/tests/strings-rules-test.smt3 b/tests/strings-rules-test.smt3
index 003f4e64..e0a1295b 100644
--- a/tests/strings-rules-test.smt3
+++ b/tests/strings-rules-test.smt3
@@ -15,10 +15,10 @@
           (string_from_flat_form U ts rev)))))
 )
 
-(declare-fun x () String)
-(declare-fun y () String)
-(declare-fun z () String)
-(declare-fun w () String)
+(declare-const x String)
+(declare-const y String)
+(declare-const z String)
+(declare-const w String)
 
 (assume @p0 (= (str.++ x y) (str.++ x z)))
 (step @q0 (= y z) :rule concat_eq :premises (@p0) :args (String false))
diff --git a/tests/substitution-opaque.smt3 b/tests/substitution-opaque.smt3
index 09e88b3c..5691ab35 100644
--- a/tests/substitution-opaque.smt3
+++ b/tests/substitution-opaque.smt3
@@ -26,8 +26,8 @@
 (declare-const and (-> Bool Bool Bool) :right-assoc-nil true)
 (declare-const not (-> Bool Bool))
 
-(declare-sort Array 2)
-(declare-sort Int 0)
+(declare-type Array (Type Type))
+(declare-type Int ())
 
 (declare-const @array_deq_diff 
   (-> 
diff --git a/tests/tiny_oracle.smt3 b/tests/tiny_oracle.smt3
index b8e637aa..4d60eebd 100644
--- a/tests/tiny_oracle.smt3
+++ b/tests/tiny_oracle.smt3
@@ -1,4 +1,4 @@
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 
 (declare-oracle-fun test_oracle (Int) Bool ./tiny_oracle.sh)
diff --git a/tests/to_string.smt3 b/tests/to_string.smt3
index 7f534093..375f0e59 100644
--- a/tests/to_string.smt3
+++ b/tests/to_string.smt3
@@ -2,13 +2,13 @@
 ; we can't do options in regression tests, these pass with:
 ; `--no-normalize-dec --no-normalize-hex`
 
-(declare-sort Real 0)
+(declare-type Real ())
 (declare-consts <rational> Real)
 ;(declare-consts <decimal> Real)
-(declare-sort BitVec 0)
+(declare-type BitVec ())
 (declare-consts <binary> BitVec)
 ;(declare-consts <hexadecimal> BitVec)
-(declare-sort String 0)
+(declare-type String ())
 (declare-consts <string> String)
 
 (declare-const ok (-> (! Type :var T :implicit) T Bool))
diff --git a/tests/typeof.smt3 b/tests/typeof.smt3
index 3002c193..2073e499 100644
--- a/tests/typeof.smt3
+++ b/tests/typeof.smt3
@@ -1,9 +1,9 @@
 (declare-const = (-> (! Type :var A :implicit) A A Bool))
 
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 
-(declare-sort Real 0)
+(declare-type Real ())
 (declare-consts <rational> Real)
 
 (declare-const to_real (-> Int Real))
diff --git a/tests/use-match.smt3 b/tests/use-match.smt3
index ef857514..055b67e2 100644
--- a/tests/use-match.smt3
+++ b/tests/use-match.smt3
@@ -20,7 +20,7 @@
     )
 )
 
-(declare-sort String 0)
+(declare-type String ())
 (declare-consts <string> String)
 (declare-const str.++ (-> String String String) :right-assoc-nil "")
 
@@ -65,5 +65,5 @@
               )
 )
 
-(declare-fun x () String)
+(declare-const x String)
 (step @p0 (= (str.++ "A" "B" x) (str.++ "AB" x)) :rule collect_acc :args ((str.++ "A" "B" x)))
diff --git a/tests/var-binders-syntax.smt3 b/tests/var-binders-syntax.smt3
index 357023d5..737ef7f8 100644
--- a/tests/var-binders-syntax.smt3
+++ b/tests/var-binders-syntax.smt3
@@ -1,5 +1,5 @@
 
-(declare-sort @List 0)
+(declare-type @List ())
 (declare-const @list.nil @List)
 (declare-const @list (-> (! Type :var T :implicit) T @List @List) :right-assoc-nil @list.nil)
 
diff --git a/user_manual.md b/user_manual.md
index 8b2b93a7..7582e1e3 100644
--- a/user_manual.md
+++ b/user_manual.md
@@ -90,12 +90,8 @@ In the following, we informally write BNF categories `<symbol>` to denote an SMT
 
 The following commands are supported for declaring and defining types and terms. The first set of commands are identical to those in SMT-LIB version 3.0:
 - `(declare-const <symbol> <type> <attr>*)` declares a constant named `<symbol>` whose type is `<type>`. Can be given an optional list of attributes (see [attributes](#attributes)).
-- `(declare-fun <symbol> (<type>*) <type> <attr>*)` declares a constant named `<symbol>` whose type is given by the argument types and return type. Can be given an optional list of attributes.
-- `(declare-sort <symbol> <numeral>)` declares a new type named `<symbol>` whose kind is `(-> Type^n Type)` if `n>0` or `Type` for the provided numeral `n`.
 - `(declare-type <symbol> (<type>*))` declares a new type named `<symbol>` whose kind is given by the argument types and return type `Type`.
-- `(define-const <symbol> <term>)` defines `<symbol>` to be the given term.
-- `(define-sort <symbol> (<symbol>*) <type>)` defines `<symbol>` to be a lambda term whose arguments are given by variables of kind `Type` and whose body is given by the return type, or the return type if the argument is empty.
-- `(define-type <symbol> (<type>*) <type>)` defines `<symbol>` to be a lambda term whose kind is given
+- `(define-type <symbol> (<type>*) <type>)` defines `<symbol>` to be a lambda term whose type is given by the argument and return types.
 - `(declare-datatype <symbol> <datatype-dec>)` defines a datatype `<symbol>`, along with its associated constructors, selectors, discriminators and updaters.
 - `(declare-datatypes (<sort-dec>^n) (<datatype-dec>^n))` defines a list of `n` datatypes for some `n>0`.
 - `(exit)` causes the checker to immediately terminate.
@@ -113,11 +109,11 @@ The ALF language contains further commands for declaring symbols that are not st
 ### Example: Basic Declarations
 
 ```
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const c Int)
 (declare-const f (-> Int Int Int))
-(declare-fun g (Int Int) Int)
-(declare-fun P (Int) Bool)
+(declare-const g (-> Int (-> Int Int)))
+(declare-const P (-> Int Bool))
 ```
 
 Since alfc does not assume any builtin definitions of SMT-LIB theories, definitions of standard symbols (such as `Int`) may be provided in ALF signatures. In the above example, `c` is declared to be a constant (0-ary) symbol of type `Int`. The symbol `f` is a function taking two integers and returning an integer.
@@ -148,20 +144,19 @@ In other words, the following file is equivalent to the one above after parsing:
 ### Example: Polymorphic types
 
 ```
-(declare-sort Int 0)
-(declare-sort Array 2)
+(declare-type Int ())
+(declare-type Array (Type Type))
 (declare-const a (Array Int Bool))
 
-(define-sort IntArray (T) (Array Int T))
+(define IntArray ((T Type)) (Array Int T))
 (declare-const b (IntArray Bool))
 ```
 
 In the above example, we define the integer sort and the array sort, whose kind is `(-> Type Type Type)`.
 
-Note the following declarations all generate terms of the same type:
+Note the following declarations generate terms of the same type:
 
 ```
-(declare-sort Array_v1 2)
 (declare-type Array_v2 (Type Type))
 (declare-const Array_v3 (-> Type Type Type))
 ```
@@ -182,7 +177,7 @@ If this is not the specified type (in this case `Bool`), an error will be thrown
 The ALF language uses the SMT-LIB version 3.0 attributes `:var <symbol>` and `:implicit` in term annotations for naming arguments of functions and specifying they are implicit.
 
 ```
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const eq (-> (! Type :var T) T T Bool))
 (define P ((x Int) (y Int)) (eq Int x y))
 ```
@@ -190,7 +185,7 @@ The ALF language uses the SMT-LIB version 3.0 attributes `:var <symbol>` and `:i
 The above example declares a predicate `eq` whose first argument is a type, that is given a name `T`. It then expects two terms of type `T` and returns a `Bool`. In the definition of `P`, this predicate is applied to two variables, where the type `Int` must be explicitly provided.
 
 ```
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const = (-> (! Type :var T :implicit) T T Bool))
 (define P ((x Int) (y Int)) (= x y))
 ```
@@ -201,7 +196,7 @@ We call `T` in the above definitions a *parameter*. The free parameters of the r
 
 
 ```
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const f (-> (! Type :var T :implicit) Int T))
 ```
 
@@ -214,7 +209,7 @@ We call `T` in the above definitions a *parameter*. The free parameters of the r
 Arguments to functions can also be annotated with the attribute `:requires (<term> <term>)` to denote a equality condition that is required for applications of the term to type check.
 
 ```
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const BitVec (-> (! Int :var w :requires ((alf.is_neg w) false)) Type))
 ```
 The above declares the integer sort and the bitvector sort that expects a non-negative integer `w`.
@@ -294,7 +289,7 @@ The nil terminator of a right associative operator may involve previously declar
 For example:
 
 ```
-(declare-sort RegLan 0)
+(declare-type RegLan ())
 (declare-const re.all RegLan)
 (declare-const re.inter (-> RegLan RegLan RegLan) :right-assoc-nil re.all)
 ```
@@ -327,8 +322,8 @@ This annotation marks that the term should be treated as a list of arguments whe
 (define Q ((x Bool) (y Bool :list)) (or x y))
 (declare-const a Bool)
 (declare-const b Bool)
-(define-const Paab Bool (P a (or a b)))
-(define-const Qaab Bool (Q a (or a b)))
+(define Paab () (P a (or a b)))
+(define Qaab () (Q a (or a b)))
 ```
 
 In the above example, note that `or` has been marked `:right-assoc-nil false`.
@@ -371,7 +366,7 @@ In contrast, `(or x)` denotes the `or` whose children are `x` and `false`.
 ### Chainable
 
 ```
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const and (-> Bool Bool Bool) :right-assoc)
 (declare-const >= (-> Int Int Bool) :chainable)
 (define ((x Int) (y Int) (z Int)) (>= x y z))
@@ -387,7 +382,7 @@ where the type of its chaining operator is `(-> S S S)`, and that operator has b
 ### Pairwise
 
 ```
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const and (-> Bool Bool Bool) :right-assoc)
 (declare-const distinct (-> (! Type :var T :implicit) T T Bool) :pairwise and)
 (define P ((x Int) (y Int) (z Int)) (distinct x y z))
@@ -399,12 +394,12 @@ where the type of its pairwise operator is `(-> S S S)`, and that operator has b
 
 ### <a name="binders"></a>Binder
 ```
-(declare-sort Int 0)
-(declare-sort @List 0)
+(declare-type Int ())
+(declare-type @List ())
 (declare-const @nil @List)
 (declare-const @cons (-> (! Type :var T :implicit) T @List @List) :right-assoc-nil @nil)
 (declare-const forall (-> @List Bool Bool) :binder @cons)
-(declare-fun P (Int) Bool)
+(declare-const P (-> Int Bool))
 
 (define Q1 () (forall ((x Int)) (P x)))
 (define Q2 () (forall ((x Int)) (P x)))
@@ -461,9 +456,9 @@ String values are implemented as a vector of unsigned integers whose maximum val
 
 The following gives an example of how to define the class of numeral constants.
 ```
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
-(declare-fun P ((x Int)) Bool (> x 7))
+(define P ((x Int)) (> x 7))
 ```
 
 In the above example, the `declare-consts` command specifies that numerals (`1`, `2`, `3`, and so on) are constants of type `Int`.
@@ -675,7 +670,7 @@ The ALF checker supports extensions of `alf.and, alf.or, alf.xor, alf.add, alf.m
 Note the following examples of core operators for the given signature
 
 ```
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const x Int)
 (declare-const y Int)
 (declare-const a Bool)
@@ -777,7 +772,7 @@ for the term `or` applied to arguments `a,b`.
 ### Example: Type rule for BitVector concatentation
 
 ```
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 (declare-type BitVec (Int))
 
@@ -788,8 +783,8 @@ for the term `or` applied to arguments `a,b`.
   (BitVec m)
   (BitVec (alf.add n m))))
 
-(declare-fun x () (BitVec 2))
-(declare-fun y () (BitVec 3))
+(declare-const x (BitVec 2))
+(declare-const y (BitVec 3))
 (define z () (concat x y) :type (BitVec 5))
 ```
 
@@ -802,8 +797,8 @@ If on the other hand we defined:
 ...
 (declare-const a Int)
 (declare-const b Int)
-(declare-fun x2 () (BitVec a))
-(declare-fun y2 () (BitVec b))
+(declare-const x2 (BitVec a))
+(declare-const y2 (BitVec b))
 (define z2 () (concat x2 y2))
 ```
 The type `z2` in the above example is `(BitVec (alf.add a b))`, where the application of `alf.add` does not evaluate.
@@ -813,13 +808,13 @@ For example, given a function `f` of type `(-> (BitVec (alf.add b a)) T)`, the t
 ### <a name="bv-literals"></a>Example: Type rule for BitVector constants
 
 ```
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 (declare-type BitVec (Int))
 
 (declare-consts <binary> (BitVec (alf.len alf.self)))
 
-(define-const x (BitVec 3) #b000)
+(define x () #b000 :type (BitVec 3))
 ```
 To define the class of binary values, whose type depends on the number of bits they contain, the ALF checker provides support for a distinguished parameter `alf.self`.
 The type checker for values applies the substitution mapping `alf.self` to the term being type checked.
@@ -837,7 +832,7 @@ Its syntax is:
 In the following example,
 we declare bitvector-or (`bvor` in SMT-LIB) where its nil terminator is bitvector zero for the given bitwidth.
 ```
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)                ; numeral literals denote Int constants
 (declare-type BitVec (Int))
 (declare-consts <binary> 
@@ -1030,9 +1025,9 @@ In detail, an application of this proof rule for premise proof `(= a b)` for con
 A list of requirements can be given to a proof rule.
 
 ```
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
-(declare-fun >= (Int Int) Bool)
+(declare-const >= (-> Int Int Bool))
 (declare-rule leq-contra ((x Int))
     :premise ((>= x 0))
     :requires (((alf.is_neg x) true))
@@ -1047,7 +1042,7 @@ It requires that the left hand side of this inequality `x` is a negative numeral
 A rule can take an arbitrary number of premises via the syntax `:premise-list <term> <term>`. For example:
 
 ```
-(declare-fun and (-> Bool Bool Bool) :right-assoc-nil true)
+(declare-const and (-> Bool Bool Bool) :right-assoc-nil true)
 (declare-rule and-intro ((F Bool))
     :premise-list F and
     :conclusion F)
@@ -1077,7 +1072,7 @@ where
     :premises ((= t s))
     :conclusion (= s t)
 )
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const a Int)
 (declare-const b Int)
 (assume @p0 (= a b))
@@ -1249,7 +1244,7 @@ Thus, the side condition is written in three cases: either `t` is `x` in which c
 ### Example: Term evaluator
 
 ```
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 (declare-const = (-> (! Type :var T :implicit) T T Bool))
 (declare-const + (-> Int Int Int))
@@ -1275,8 +1270,8 @@ The above example recursively evaluates arithmetic terms and predicates accordin
 ### Example: A computational type rule
 
 ```
-(declare-sort Int 0)
-(declare-sort Real 0)
+(declare-type Int ())
+(declare-type Real ())
 (program arith.typeunion ()
     (Type Type) Type
     (
@@ -1298,7 +1293,7 @@ The return type of `+` invokes this side condition, which conceptually is implem
 ### Example: Conversion to DIMACS
 
 ```
-(declare-sort String 0)
+(declare-type String ())
 (declare-consts <string> String)
 (declare-const not (-> Bool Bool))
 (declare-const or (-> Bool Bool Bool) :right-assoc-nil false)
@@ -1346,7 +1341,7 @@ Also, similar to programs, the free parameters of `ri` that occur in the paramet
 ### Examples of legal and illegal match terms
 
 ```
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const F Bool)
 (declare-const a Int)
 (declare-const P (-> Int Bool))
@@ -1387,7 +1382,7 @@ Also, similar to programs, the free parameters of `ri` that occur in the paramet
 ### Example: Proof rule for symmetry of (dis)equality
 
 ```
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const = (-> (! Type :var T :implicit) T T Bool))
 (declare-const not (-> Bool Bool))
 (declare-rule symm ((F Bool))
@@ -1406,7 +1401,7 @@ It matches the given premise `F` with either `(= t1 t2)` or `(not (= t1 t2))` an
 
 Internally, the semantics of `alf.match` can be seen as an (inlined) program applied to its head, such that the above example is equivalent to:
 ```
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const = (-> (! Type :var T :implicit) T T Bool))
 (declare-const not (-> Bool Bool))
 (program matchF ((t1 Int) (t2 Int))
@@ -1429,7 +1424,7 @@ In more general cases, if the body of the match term contains free variables, th
 ### Example: Proof rule for transitivity of equality with a premise list
 
 ```
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-const = (-> (! Type :var T :implicit) T T Bool))
 (declare-const and (-> Bool Bool Bool) :left-assoc)
 
@@ -1485,8 +1480,8 @@ For this reason, alfc additionally supports providing an optional normalization
 
 For example:
 ```
-(declare-sort Int 0)
-(declare-sort Real 0)
+(declare-type Int ())
+(declare-type Real ())
 (declare-const / (-> Int Int Real))
 (program normalize ((T Type) (S Type) (f (-> S T)) (x S) (a Int) (b Int))
    (T) T
@@ -1512,14 +1507,14 @@ In particular, the ALF checker supports the command:
 ```
 (declare-oracle-fun <symbol> (<type>*) <type> <symbol>)
 ```
-Like `declare-fun`, this command declares a constant named `<symbol>` whose type is given by the argument types and return type.
+Like the `declare-fun` command from SMT-LIB, this command declares a constant named `<symbol>` whose type is given by the argument types and return type.
 In addition, a symbol is provided at the end of the command which specifies the name of executable command to run.
 Ground applications of oracle functions are eagerly evaluated by invoking the binary and parsing its result, which we describe in more detail in the following.
 
 ### Example: Oracle isPrime
 
 ```
-(declare-sort Int 0)
+(declare-type Int ())
 (declare-consts <numeral> Int)
 (declare-const = (-> (! Type :var T :implicit) T T Bool))
 (declare-const >= (-> Int Int Bool))
@@ -1593,10 +1588,6 @@ Valid inputs to the ALF checker are `<alf-command>*`, where:
     (declare-const <symbol> <type> <attr>*)
     (declare-datatype <symbol> <datatype-dec>) |
     (declare-datatypes (<sort-dec>^n) (<datatype-dec>^n)) |
-    (declare-fun <symbol> (<type>*) <type> <attr>*) |
-    (declare-sort <symbol> <numeral>) |
-    (define-const <symbol> <term>) |
-    (define-sort <symbol> (<symbol>*) <type>) |
     (echo <string>?) |
     (exit) |
     (reset)
@@ -1606,7 +1597,11 @@ Valid inputs to the ALF checker are `<alf-command>*`, where:
     (assert <term>) |
     (check-sat) |
     (check-sat-assuming (<term>*)) |
+    (declare-fun <symbol> (<type>*) <type> <attr>*) |
+    (declare-sort <symbol> <numeral>) |
+    (define-const <symbol> <term>) |
     (define-fun <symbol> (<typed-param>*) <type> <term>) |
+    (define-sort <symbol> (<symbol>*) <type>) |
     (set-info <attr>) |
     (set-logic <symbol>) |
     (set-option <attr>) |