--- a/src/HOL/ex/mesontest2.ML Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/ex/mesontest2.ML Thu Oct 12 18:38:23 2000 +0200
@@ -11,9 +11,9 @@
(*All but the fastest are ignored to reduce build time*)
val even_hard_ones = false;
-(*Prod.thy instead of HOL.thy regards arguments as tuples.
+(*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 Prod.thy s (fn [] => [tac]);
+fun prove (s,tac) = prove_goal Product_Type.thy s (fn [] => [tac]);
fun prove_hard arg = if even_hard_ones then prove arg else TrueI;