# HG changeset patch
# User blanchet
# Date 1357220465 -3600
# Node ID 70c2a6d513fd956533da53d1331d82176255acdc
# Parent  054f6bf349d265a41d08b5225ce00f09894c02de
tuned comment

diff -r 054f6bf349d2 -r 70c2a6d513fd src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Thu Jan 03 14:23:10 2013 +0100
+++ b/src/HOL/Tools/Meson/meson.ML	Thu Jan 03 14:41:05 2013 +0100
@@ -168,8 +168,8 @@
   in  tryall rls  end;
 
 (* Special version of "rtac" that works around an explosion in the unifier.
-   If the goal has the form "?P c", the danger is that unifying "?P" with a
-   formula of the form "... c ... c ... c ..." will lead to a huge unification
+   If the goal has the form "?P c", the danger is that resolving it against a
+   property of the form "... c ... c ... c ..." will lead to a huge unification
    problem, due to the (spurious) choices between projection and imitation. The
    workaround is to instantiate "?P := (%c. ... c ... c ... c ...)" manually. *)
 fun quant_rtac th i st =