# HG changeset patch
# User wenzelm
# Date 1256765160 -3600
# Node ID 4645818f0fbd9e2562e34079885d9672c3ac78a0
# Parent  affe60b3d8642f2328502679d7df759cccd928b4
updated Isar.goal;

diff -r affe60b3d864 -r 4645818f0fbd doc-src/IsarImplementation/Thy/Integration.thy
--- a/doc-src/IsarImplementation/Thy/Integration.thy	Wed Oct 28 22:18:00 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Integration.thy	Wed Oct 28 22:26:00 2009 +0100
@@ -274,7 +274,8 @@
   @{index_ML Isar.state: "unit -> Toplevel.state"} \\
   @{index_ML Isar.exn: "unit -> (exn * string) option"} \\
   @{index_ML Isar.context: "unit -> Proof.context"} \\
-  @{index_ML Isar.goal: "unit -> thm"} \\
+  @{index_ML Isar.goal: "unit ->
+  {context: Proof.context, facts: thm list, goal: thm}"} \\
   \end{mldecls}
 
   \begin{description}
@@ -293,8 +294,9 @@
   "Isar.state ()"}, analogous to @{ML Context.proof_of}
   (\secref{sec:generic-context}).
 
-  \item @{ML "Isar.goal ()"} picks the tactical goal from @{ML
-  "Isar.state ()"}, represented as a theorem according to
+  \item @{ML "Isar.goal ()"} produces the full Isar goal state,
+  consisting of proof context, facts that have been indicated for
+  immediate use, and the tactical goal according to
   \secref{sec:tactical-goals}.
 
   \end{description}
diff -r affe60b3d864 -r 4645818f0fbd doc-src/IsarImplementation/Thy/document/Integration.tex
--- a/doc-src/IsarImplementation/Thy/document/Integration.tex	Wed Oct 28 22:18:00 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Integration.tex	Wed Oct 28 22:26:00 2009 +0100
@@ -335,7 +335,8 @@
   \indexdef{}{ML}{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\
   \indexdef{}{ML}{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
   \indexdef{}{ML}{Isar.context}\verb|Isar.context: unit -> Proof.context| \\
-  \indexdef{}{ML}{Isar.goal}\verb|Isar.goal: unit -> thm| \\
+  \indexdef{}{ML}{Isar.goal}\verb|Isar.goal: unit ->|\isasep\isanewline%
+\verb|  {context: Proof.context, facts: thm list, goal: thm}| \\
   \end{mldecls}
 
   \begin{description}
@@ -353,7 +354,9 @@
   \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()|, analogous to \verb|Context.proof_of|
   (\secref{sec:generic-context}).
 
-  \item \verb|Isar.goal ()| picks the tactical goal from \verb|Isar.state ()|, represented as a theorem according to
+  \item \verb|Isar.goal ()| produces the full Isar goal state,
+  consisting of proof context, facts that have been indicated for
+  immediate use, and the tactical goal according to
   \secref{sec:tactical-goals}.
 
   \end{description}%