diff -r e7fb7ef2a85e -r 0c6c943d8f1e src/HOL/ex/Meson_Test.thy
--- a/src/HOL/ex/Meson_Test.thy	Thu Aug 02 22:43:47 2007 +0200
+++ b/src/HOL/ex/Meson_Test.thy	Thu Aug 02 23:18:13 2007 +0200
@@ -86,6 +86,8 @@
 by (best_prolog_tac size_of_subgoals horns43);   (*1.6 secs*)
 *}
 
+ML {* Logic.auto_rename := false; *}
+
 (*
 #1  (q x xa ==> ~ q x xa) ==> q xa x
 #2  (q xa x ==> ~ q xa x) ==> q x xa