-\newcommand*\PROP{PROP}
-\newcommand*\CROP[1]{CROP}
-\newcommand*\TYPE[1]{TYPE}
-\newcommand*\LREF[2]{#1}
-\newcommand*\GREF[2]{#1}
-\newcommand*\ABBR[3]{(D #1 #2 #3) }
-\newcommand*\ABST[2]{(I #1 #2) }
-\newcommand*\PROD[2]{(P #1 #2) }
-\newcommand*\APPL{(A)\ma@next\ma@space\ma@arg\ma@space\relax}
-\newcommand*\CASE[3]{(C #1 #2 #3)\ma@next\ma@space\ma@arg\ma@space\relax}
+\newcommand*\PROP{\mathord\mathrm{PROP}}
+\newcommand*\CROP[1]{\mathord\mathrm{CROP}}
+\newcommand*\TYPE[1]{\mathord\mathrm{TYPE}}
+\newcommand*\LREF[2]{\ma@setoptlink{#1}{#2}}
+\newcommand*\GREF[2]{\ma@setoptlink{\mathrm{#1}}{#2}}
+\newcommand*\ABBR[4]{\ma@op\ma@setopttarget{#1}{#2}\ma@abbr #4\ma@cast #3\ma@cp\ma@bind}
+\newcommand*\ABST[3]{\ma@op\ma@setopttarget{#1}{#2}\ma@cast #3\ma@cp\ma@bind}
+\newcommand*\PROD[3]{\def\ma@tmp{#2}%
+ \ifx\ma@tmp\empty #3\ma@arrw\else
+ \ma@op\ma@prod\ma@setopttarget{#1}{#2}\ma@cast #3\ma@cp\ma@bind\fi
+}
+\newcommand*\FALL[3]{\def\ma@tmp{#2}%
+ \ifx\ma@tmp\empty #3\ma@impl\else
+ \ma@op\ma@fall\ma@setopttarget{#1}{#2}\ma@cast #3\ma@cp\ma@bind\fi
+}
+\newcommand*\APPL[1]{#1\ma@args}
+\newcommand*\CASE[3]{#3\ma@case\ma@cases}
+\newcommand*\CAZE[3]{#3\ma@caze\ma@op\ma@qm\ma@cast #2\ma@cp\ma@cases}
+\newcommand*\PAIR[2]{#1\ma@pair #2}