src/CCL/Set.ML

--- a/src/CCL/Set.ML	Tue Jul 14 13:33:12 1998 +0200
+++ b/src/CCL/Set.ML	Wed Jul 15 10:15:13 1998 +0200
@@ -116,7 +116,7 @@
 qed_goal "subset_refl" Set.thy "A <= A"
  (fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]);
 
-Goal "!!A B C. [| A<=B;  B<=C |] ==> A<=C";
+Goal "[| A<=B;  B<=C |] ==> A<=C";
 by (rtac subsetI 1);
 by (REPEAT (eresolve_tac [asm_rl, subsetD] 1));
 qed "subset_trans";