--- a/src/HOL/ex/set.ML Mon Nov 03 21:56:59 1997 +0100
+++ b/src/HOL/ex/set.ML Tue Nov 04 09:26:15 1997 +0100
@@ -9,7 +9,7 @@
writeln"File HOL/ex/set.";
-set_current_thy"Set";
+context Set.thy;
(*Nice demonstration of blast_tac--and its overloading problems*)
goal Set.thy "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
--- a/src/ZF/ex/misc.ML Mon Nov 03 21:56:59 1997 +0100
+++ b/src/ZF/ex/misc.ML Tue Nov 04 09:26:15 1997 +0100
@@ -14,7 +14,7 @@
by (Blast_tac 1);
result();
-set_current_thy"Perm";
+context Perm.thy;
(*Example 12 (credited to Peter Andrews) from
W. Bledsoe. A Maximal Method for Set Variables in Automatic Theorem-proving.