tuned comment
authorblanchet
Thu Jan 03 14:41:05 2013 +0100 (2013-01-03)
changeset 5070270c2a6d513fd
parent 50701 054f6bf349d2
child 50703 76a2e506c125
tuned comment
src/HOL/Tools/Meson/meson.ML
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Thu Jan 03 14:23:10 2013 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Thu Jan 03 14:41:05 2013 +0100
     1.3 @@ -168,8 +168,8 @@
     1.4    in  tryall rls  end;
     1.5  
     1.6  (* Special version of "rtac" that works around an explosion in the unifier.
     1.7 -   If the goal has the form "?P c", the danger is that unifying "?P" with a
     1.8 -   formula of the form "... c ... c ... c ..." will lead to a huge unification
     1.9 +   If the goal has the form "?P c", the danger is that resolving it against a
    1.10 +   property of the form "... c ... c ... c ..." will lead to a huge unification
    1.11     problem, due to the (spurious) choices between projection and imitation. The
    1.12     workaround is to instantiate "?P := (%c. ... c ... c ... c ...)" manually. *)
    1.13  fun quant_rtac th i st =