# HG changeset patch
# User paulson
# Date 855913128 -3600
# Node ID 99df9182f5a5f8cc60f788d5281b76d8f4333d42
# Parent  0b136448121456be66f095911f6fabcf0dd0db8d
Tidying and a corrected comment

diff -r 0b1364481214 -r 99df9182f5a5 src/HOL/ex/mesontest.ML
--- a/src/HOL/ex/mesontest.ML	Fri Feb 14 10:36:33 1997 +0100
+++ b/src/HOL/ex/mesontest.ML	Fri Feb 14 10:38:48 1997 +0100
@@ -508,11 +508,11 @@
 
 (*The Los problem?  Circulated by John Harrison*)
 goal HOL.thy "(! x y z. P x y & P y z --> P x z) &      \
-\      (! x y z. Q x y & Q y z --> Q x z) &     \
-\      (! x y. P x y --> P y x) &       \
-\      (! (x::'a) y. P x y | Q x y)     \
+\      (! x y z. Q x y & Q y z --> Q x z) &             \
+\      (! x y. P x y --> P y x) &                       \
+\      (! x y. P x y | Q x y)                           \
 \      --> (! x y. P x y) | (! x y. Q x y)";
-by (safe_best_meson_tac 1);     (*3 secs; iter. deepening is VERY slow*)
+by (safe_best_meson_tac 1);     (*2.3 secs; iter. deepening is VERY slow*)
 result();
 
 (*A similar example, suggested by Johannes Schumann and credited to Pelletier*)