src/HOL/ex/Meson_Test.thy

--- a/src/HOL/ex/Meson_Test.thy	Fri Jul 24 21:34:37 2009 +0200
+++ b/src/HOL/ex/Meson_Test.thy	Fri Jul 24 22:09:09 2009 +0200
@@ -5,7 +5,11 @@
 imports Main
 begin
 
-ML {* open OldGoals *}
+ML {*
+  val Goal = OldGoals.Goal;
+  val by = OldGoals.by;
+  val gethyps = OldGoals.gethyps;
+*}
 
 text {*
   WARNING: there are many potential conflicts between variables used