--- a/src/HOL/ex/Meson_Test.thy Fri Jul 24 20:55:56 2009 +0200
+++ b/src/HOL/ex/Meson_Test.thy Fri Jul 24 21:02:34 2009 +0200
@@ -5,6 +5,8 @@
imports Main
begin
+ML {* open OldGoals *}
+
text {*
WARNING: there are many potential conflicts between variables used
below and constants declared in HOL!