src/HOL/ex/mesontest2.ML
changeset 10440 2074e62da354
parent 10212 33fe2d701ddd
child 11451 8abfb4f7bd02
--- a/src/HOL/ex/mesontest2.ML	Fri Nov 10 19:07:17 2000 +0100
+++ b/src/HOL/ex/mesontest2.ML	Fri Nov 10 19:08:30 2000 +0100
@@ -11,9 +11,7 @@
 (*All but the fastest are ignored to reduce build time*)
 val even_hard_ones = false;
 
-(*Product_Type.thy instead of HOL.thy regards arguments as tuples.
-  But Main.thy would allow clashes with many other constants*)
-fun prove (s,tac) = prove_goal Product_Type.thy s (fn [] => [tac]);
+fun prove (s,tac) = prove_goal (the_context ()) s (fn [] => [tac]);
 
 fun prove_hard arg = if even_hard_ones then prove arg else TrueI;