# HG changeset patch
# User paulson
# Date 1376994987 -3600
# Node ID bc129252bba0efd898b7011f6033d65f84a56566
# Parent  667717a5ad806b0b5140aa7d956e5d3098021339# Parent  e79afad81386641da86c24e203423279112bb5c9
merged

diff -r 667717a5ad80 -r bc129252bba0 src/Doc/IsarImplementation/Tactic.thy
--- a/src/Doc/IsarImplementation/Tactic.thy	Tue Aug 20 11:42:52 2013 +0200
+++ b/src/Doc/IsarImplementation/Tactic.thy	Tue Aug 20 11:36:27 2013 +0100
@@ -336,13 +336,15 @@
   \item @{ML match_tac}, @{ML ematch_tac}, @{ML dmatch_tac}, and @{ML
   bimatch_tac} are similar to @{ML resolve_tac}, @{ML eresolve_tac},
   @{ML dresolve_tac}, and @{ML biresolve_tac}, respectively, but do
-  not instantiate schematic variables in the goal state.
+  not instantiate schematic variables in the goal state.%
+\footnote{Strictly speaking, matching means to treat the unknowns in the goal
+  state as constants, but these tactics merely discard unifiers that would
+  update the goal state. In rare situations (where the conclusion and 
+  goal state have flexible terms at the same position), the tactic
+  will fail even though an acceptable unifier exists.}
+  These tactics were written for a specific application within the classical reasoner.
 
   Flexible subgoals are not updated at will, but are left alone.
-  Strictly speaking, matching means to treat the unknowns in the goal
-  state as constants; these tactics merely discard unifiers that would
-  update the goal state.
-
   \end{description}
 *}