# HG changeset patch
# User wenzelm
# Date 878631975 -3600
# Node ID b131edcfeac3c4ffde6518ce0ab51e921aac3d62
# Parent  1610602a2964a85ca8f2c8a2464f941e4ff34ca7
isatool fixclasimp;

diff -r 1610602a2964 -r b131edcfeac3 src/HOL/ex/set.ML
--- 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}";
diff -r 1610602a2964 -r b131edcfeac3 src/ZF/ex/misc.ML
--- 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.