@@ -203,7 +203,8 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
203203 case lookupCtxtExact n (idris_datatypes ist) of
204204 Just t -> do
205205 let others = hints ++ con_names t ++ autohints
206− when (not fromProver) -- in interactive mode,
206+ when (not fromProver && length (con_names t) > 1)
207+ -- in interactive mode,
207208 -- don't just guess (fine for 'auto',
208209 -- since that's part of the point...)
209210 $ checkConstructor ist others