# HG changeset patch
# User paulson
# Date 855912906 -3600
# Node ID a5b6a632768d6642f84b277658f55b6faa8e768f
# Parent  655dc064a28ca9037b774661c7dca6e5b46e8b19
Strengthened warnings concerning topthm(), etc.

diff -r 655dc064a28c -r a5b6a632768d doc-src/Ref/goals.tex
--- a/doc-src/Ref/goals.tex	Fri Feb 14 10:34:24 1997 +0100
+++ b/doc-src/Ref/goals.tex	Fri Feb 14 10:35:06 1997 +0100
@@ -527,8 +527,10 @@
 
 \section{Debugging and inspecting}
 \index{tactics!debugging}
-These specialized operations support the debugging of tactics.  They refer
-to the current proof state of the subgoal module.
+These functions can be useful when you are debugging a tactic.  They refer
+to the current proof state stored in the subgoal module.  A tactic
+should never call them; it should operate on the proof state supplied as its
+argument.
 
 \subsection{Reading and printing terms}
 \index{terms!reading of}\index{terms!printing of}\index{types!printing of}
@@ -576,6 +578,7 @@
   command is supplied for debugging uses of \ttindex{METAHYPS}.
 \end{ttdescription}
 
+
 \subsection{Filtering lists of rules}
 \begin{ttbox} 
 filter_goal: (term*term->bool) -> thm list -> int -> thm list