--- a/src/HOL/IsaMakefile Fri Nov 10 19:07:17 2000 +0100
+++ b/src/HOL/IsaMakefile Fri Nov 10 19:08:30 2000 +0100
@@ -462,8 +462,8 @@
ex/Primrec.thy ex/Puzzle.ML ex/Puzzle.thy ex/Qsort.ML ex/Qsort.thy \
ex/ROOT.ML ex/Recdefs.ML ex/Recdefs.thy ex/Records.thy ex/Ring.ML \
ex/Ring.thy ex/StringEx.ML ex/StringEx.thy ex/Tarski.ML \
- ex/Tarski.thy ex/Tuple.thy ex/cla.ML ex/mesontest.ML \
- ex/mesontest2.ML ex/set.ML ex/set.thy ex/svc_test.ML ex/svc_test.thy
+ ex/Tarski.thy ex/Tuple.thy ex/cla.ML ex/mesontest.ML ex/mesontest2.ML \
+ ex/mesontest2.thy ex/set.ML ex/set.thy ex/svc_test.ML ex/svc_test.thy
@$(ISATOOL) usedir $(OUT)/HOL ex
--- a/src/HOL/ex/ROOT.ML Fri Nov 10 19:07:17 2000 +0100
+++ b/src/HOL/ex/ROOT.ML Fri Nov 10 19:08:30 2000 +0100
@@ -11,7 +11,7 @@
time_use_thy "NatSum";
time_use "cla.ML";
time_use "mesontest.ML";
-time_use "mesontest2.ML";
+time_use_thy "mesontest2";
time_use_thy "BT";
time_use_thy "AVL";
time_use_thy "InSort";
--- 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;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/mesontest2.thy Fri Nov 10 19:08:30 2000 +0100
@@ -0,0 +1,9 @@
+
+(*Theory Product_Type instead of HOL regards arguments as tuples.
+ But theory Main would allow clashes with many other constants.*)
+
+theory mesontest2 = Product_Type:
+
+hide const inverse divide
+
+end