diff -r 5f462dfaf130 -r 5c7a69cef18b Set.ML
--- a/Set.ML	Fri Jun 24 15:11:39 1994 +0200
+++ b/Set.ML	Wed Jun 29 12:04:04 1994 +0200
@@ -117,10 +117,10 @@
 (*Takes assumptions A<=B; c:A and creates the assumption c:B *)
 fun set_mp_tac i = etac subsetCE i  THEN  mp_tac i;
 
-val subset_refl = prove_goal Set.thy "A <= A::'a set"
+val subset_refl = prove_goal Set.thy "A <= (A::'a set)"
  (fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]);
 
-val prems = goal Set.thy "[| A<=B;  B<=C |] ==> A<=C::'a set";
+val prems = goal Set.thy "[| A<=B;  B<=C |] ==> A<=(C::'a set)";
 by (cut_facts_tac prems 1);
 by (REPEAT (ares_tac [subsetI] 1 ORELSE set_mp_tac 1));
 val subset_trans = result();
@@ -129,25 +129,25 @@
 (*** Equality ***)
 
 (*Anti-symmetry of the subset relation*)
-val prems = goal Set.thy "[| A <= B;  B <= A |] ==> A = B::'a set";
+val prems = goal Set.thy "[| A <= B;  B <= A |] ==> A = (B::'a set)";
 by (rtac (iffI RS set_ext) 1);
 by (REPEAT (ares_tac (prems RL [subsetD]) 1));
 val subset_antisym = result();
 val equalityI = subset_antisym;
 
 (* Equality rules from ZF set theory -- are they appropriate here? *)
-val prems = goal Set.thy "A = B ==> A<=B::'a set";
+val prems = goal Set.thy "A = B ==> A<=(B::'a set)";
 by (resolve_tac (prems RL [subst]) 1);
 by (rtac subset_refl 1);
 val equalityD1 = result();
 
-val prems = goal Set.thy "A = B ==> B<=A::'a set";
+val prems = goal Set.thy "A = B ==> B<=(A::'a set)";
 by (resolve_tac (prems RL [subst]) 1);
 by (rtac subset_refl 1);
 val equalityD2 = result();
 
 val prems = goal Set.thy
-    "[| A = B;  [| A<=B; B<=A::'a set |] ==> P |]  ==>  P";
+    "[| A = B;  [| A<=B; B<=(A::'a set) |] ==> P |]  ==>  P";
 by (resolve_tac prems 1);
 by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
 val equalityE = result();