src/HOL/ex/Meson_Test.thy
changeset 32178 0261c3eaae41
parent 32174 9036cc8ae775
child 32262 73cd8f74cf2a
     1.1 --- a/src/HOL/ex/Meson_Test.thy	Fri Jul 24 21:34:37 2009 +0200
     1.2 +++ b/src/HOL/ex/Meson_Test.thy	Fri Jul 24 22:09:09 2009 +0200
     1.3 @@ -5,7 +5,11 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -ML {* open OldGoals *}
     1.8 +ML {*
     1.9 +  val Goal = OldGoals.Goal;
    1.10 +  val by = OldGoals.by;
    1.11 +  val gethyps = OldGoals.gethyps;
    1.12 +*}
    1.13  
    1.14  text {*
    1.15    WARNING: there are many potential conflicts between variables used