# HG changeset patch
# User wenzelm
# Date 973879710 -3600
# Node ID 2074e62da3548a096c19ed325fb3fb2881843ce4
# Parent  be2dc95dfe98afbbeffa93128d05c93299311362
proper theory context for mesontest2;

diff -r be2dc95dfe98 -r 2074e62da354 src/HOL/IsaMakefile
--- 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
 
 
diff -r be2dc95dfe98 -r 2074e62da354 src/HOL/ex/ROOT.ML
--- 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";
diff -r be2dc95dfe98 -r 2074e62da354 src/HOL/ex/mesontest2.ML
--- 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;
 
diff -r be2dc95dfe98 -r 2074e62da354 src/HOL/ex/mesontest2.thy
--- /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