# HG changeset patch
# User wenzelm
# Date 1283553081 -7200
# Node ID 976af4e27cde26a750606f0ed55adfdf27cddba6
# Parent  93a7365fb4ee504cbe37afed67e95516f51b5251
recovered options for goal antiquotations from f45d332a90e3: actually pass context to Proof.pretty_goals (see also 45facd8f358e);

diff -r 93a7365fb4ee -r 976af4e27cde src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Sep 03 23:54:48 2010 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Sep 04 00:31:21 2010 +0200
@@ -370,11 +370,11 @@
 
 fun pretty_goals main state =
   let
-    val (ctxt, (_, goal)) = get_goal state;
-    val ctxt' = ctxt
+    val (_, (_, goal)) = get_goal state;
+    val ctxt = context_of state
       |> Config.put Goal_Display.show_main_goal main
       |> Config.put Goal_Display.goals_total false;
-  in Goal_Display.pretty_goals ctxt' goal end;
+  in Goal_Display.pretty_goals ctxt goal end;
 
 
 
diff -r 93a7365fb4ee -r 976af4e27cde src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Fri Sep 03 23:54:48 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sat Sep 04 00:31:21 2010 +0200
@@ -583,7 +583,8 @@
 
 fun goal_state name main_goal = antiquotation name (Scan.succeed ())
   (fn {state, context = ctxt, ...} => fn () => output ctxt
-    [Pretty.chunks (Proof.pretty_goals main_goal (proof_state state))]);
+    [Pretty.chunks
+      (Proof.pretty_goals main_goal (Proof.map_context (K ctxt) (proof_state state)))]);
 
 in