Improvement for 'auto'

Now proof search can be deferred if there are too many metavariables in
the goal - previously in this case it would happily pick any old
solution causing weird errors elsewhere in some cases.