src/HOL/Tools/Meson/meson.ML
changeset 50702 70c2a6d513fd
parent 50695 cace30ea5a2c
child 51717 9e7d1c139569
     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 =