changeset 32178 | 0261c3eaae41 |
parent 32174 | 9036cc8ae775 |
child 32262 | 73cd8f74cf2a |
--- 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