diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
index eb322bbe9..4249c850a 100644
--- a/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
@@ -46,6 +46,7 @@ module Lang.Crucible.Syntax.Concrete
   , BoundedNat(..)
   , PosNat
   , posNat
+  , someAssign
   -- * Rules for pretty-printing language syntax
   , printExpr
   )
@@ -1935,26 +1936,33 @@ deriving instance Show (ACFG ext)
 
 data Arg t = Arg AtomName Position (TypeRepr t)
 
-
-
-arguments' :: forall m ext
-            . ( MonadSyntax Atomic m, ?parserHooks :: ParserHooks ext )
-           => m (Some (Ctx.Assignment Arg))
-arguments' = call (go (Some Ctx.empty))
+someAssign ::
+  forall m ext a.
+  ( MonadSyntax Atomic m
+  , ?parserHooks :: ParserHooks ext
+  ) =>
+  Text ->
+  m (Some a) ->
+  m (Some (Ctx.Assignment a))
+someAssign desc sub = call (go (Some Ctx.empty))
   where
-    go ::  Some (Ctx.Assignment Arg) -> m (Some (Ctx.Assignment Arg))
+    go :: Some (Ctx.Assignment a) -> m (Some (Ctx.Assignment a))
     go args@(Some prev) =
-      describe "argument list" $
+      describe desc $
         (emptyList *> pure args) <|>
-        (depCons oneArg $
+        (depCons sub $
            \(Some a) ->
              go (Some $ Ctx.extend prev a))
 
-      where oneArg =
-              (describe "argument" $
-               located $
-               cons atomName (cons isType emptyList)) <&>
-              \(Posd loc (x, (Some t, ()))) -> Some (Arg x loc t)
+arguments' :: forall m ext
+            . ( MonadSyntax Atomic m, ?parserHooks :: ParserHooks ext )
+           => m (Some (Ctx.Assignment Arg))
+arguments' = someAssign "argument list" oneArg
+  where oneArg =
+          (describe "argument" $
+           located $
+           cons atomName (cons isType emptyList)) <&>
+          \(Posd loc (x, (Some t, ()))) -> Some (Arg x loc t)
 
 
 saveArgs :: (MonadState (SyntaxState s) m, MonadError (ExprErr s) m)