# HG changeset patch
# User aspinall
# Date 1100632814 -3600
# Node ID 1d2dba93ef08a7452089a52b39bc57046c22ea44
# Parent  9d49290ed885822f196abb44a33bf2dd88bb2134
Markup obtain as introducing a nested goal.

diff -r 9d49290ed885 -r 1d2dba93ef08 src/Pure/proof_general.ML
--- 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)