diff --git a/saw-core/src/Verifier/SAW/Typechecker.hs b/saw-core/src/Verifier/SAW/Typechecker.hs
index 189cac71da..6beb06f728 100644
--- a/saw-core/src/Verifier/SAW/Typechecker.hs
+++ b/saw-core/src/Verifier/SAW/Typechecker.hs
@@ -113,7 +113,7 @@ inferResolveNameApp n args =
          typeInferComplete (DataTypeApp (dtName dt) params ixs)
        (_, Just (ResolvedDef d)) ->
          do t <- liftTCM scGlobalDef (defIdent d)
-            f <- typeInferComplete t
+            f <- TypedTerm t <$> liftTCM scTypeOf t
             inferApplyAll f args
        (Nothing, Nothing) ->
          throwTCError $ UnboundName n