src/HOL/ex/mesontest2.ML
changeset 10212 33fe2d701ddd
parent 9841 ca3173f87b5c
child 10440 2074e62da354
--- 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;