Markup obtain as introducing a nested goal.
--- a/src/Pure/proof_general.ML Mon Nov 15 18:21:34 2004 +0100
+++ b/src/Pure/proof_general.ML Tue Nov 16 20:20:14 2004 +0100
@@ -911,7 +911,7 @@
| "proof-chain" => markup "proofstep"
| "proof-decl" => markup "proofstep"
| "proof-asm" => markup "proofstep"
- | "proof-asm-goal" => markup "proofstep"
+ | "proof-asm-goal" => (markup "opengoal") @ (empty "openblock") (* nested proof: obtain *)
| "qed" => xmls_of_qed (name,markup)
| "qed-block" => xmls_of_qed (name,markup)
| "qed-global" => xmls_of_qed (name,markup)