diff -r f947332d5465 -r fbdb0b541314 src/CCL/Set.ML
--- a/src/CCL/Set.ML	Mon Jun 22 15:09:59 1998 +0200
+++ b/src/CCL/Set.ML	Mon Jun 22 15:18:02 1998 +0200
@@ -116,7 +116,7 @@
 qed_goal "subset_refl" Set.thy "A <= A"
  (fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]);
 
-goal Set.thy "!!A B C. [| A<=B;  B<=C |] ==> A<=C";
+Goal "!!A B C. [| A<=B;  B<=C |] ==> A<=C";
 by (rtac subsetI 1);
 by (REPEAT (eresolve_tac [asm_rl, subsetD] 1));
 qed "subset_trans";
@@ -163,7 +163,7 @@
 by (REPEAT (resolve_tac (refl::prems) 1));
 qed "setup_induction";
 
-goal Set.thy "{x. x:A} = A";
+Goal "{x. x:A} = A";
 by (REPEAT (ares_tac [equalityI,subsetI,CollectI] 1  ORELSE etac CollectD 1));
 qed "trivial_set";
 
@@ -234,7 +234,7 @@
 
 (*** Empty sets ***)
 
-goalw Set.thy [empty_def] "{x. False} = {}";
+Goalw [empty_def] "{x. False} = {}";
 by (rtac refl 1);
 qed "empty_eq";
 
@@ -252,7 +252,7 @@
 
 (*** Singleton sets ***)
 
-goalw Set.thy [singleton_def] "a : {a}";
+Goalw [singleton_def] "a : {a}";
 by (rtac CollectI 1);
 by (rtac refl 1);
 qed "singletonI";