# HG changeset patch
# User wenzelm
# Date 1213800921 -7200
# Node ID 3c17b824650bac966752fe90a0d23fb82723c2f8
# Parent  e5787c5be196d5af1e545f54446d5cdae142f797
pervasive cut_inst_tac;

diff -r e5787c5be196 -r 3c17b824650b doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Tue Jun 17 04:19:50 2008 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy	Wed Jun 18 16:55:21 2008 +0200
@@ -318,7 +318,7 @@
   assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in
   \cite[\S3]{isabelle-ref}.  Note that the scope of schematic
   variables is spread over the main goal statement.  Instantiations
-  may be given as well, see also ML tactic @{ML Tactic.cut_inst_tac}
+  may be given as well, see also ML tactic @{ML cut_inst_tac}
   in \cite[\S3]{isabelle-ref}.
 
   \item [@{method thin_tac}~@{text \<phi>}] deletes the specified