How do I remove duplicate subgoals in Isabelle?

Question

In Isabelle, one occasionally reaches a scenario where there are duplicate subgoals. For example, imagine the following proof script:

lemma "a ∧ a"
  apply (rule conjI)

with goals:

proof (prove): step 1

goal (2 subgoals):
 1. a
 2. a    

Is there any way to eliminate the duplicate subgoal in-place, so proofs need not be repeated?

Answer 1

The ML-level tactic distinct_subgoals_tac in Pure/tactic.ML removes duplicate subgoals, and can be used as follows:

lemma "a ∧ a"
  apply (rule conjI)
  apply (tactic {* distinct_subgoals_tac *})

leaving:

proof (prove): step 2

goal (1 subgoal):
 1. a

There does not appear to be a way without dropping into the ML world, unfortunately.