diff --git a/src/Lean/Widget/InteractiveGoal.lean b/src/Lean/Widget/InteractiveGoal.lean
index 556abe4d1c..49d13199b5 100644
--- a/src/Lean/Widget/InteractiveGoal.lean
+++ b/src/Lean/Widget/InteractiveGoal.lean
@@ -14,7 +14,7 @@ open Server
 
 structure InteractiveHypothesis where
   names : Array String
-  fvarIds : Array FVarId
+  fvarIds? : Option (Array FVarId)
   type : CodeWithInfos
   val? : Option CodeWithInfos := none
   isInstance : Bool