src/HOL/Set.ML

--- a/src/HOL/Set.ML	Mon Sep 06 22:12:08 1999 +0200
+++ b/src/HOL/Set.ML	Tue Sep 07 10:40:58 1999 +0200
@@ -466,7 +466,7 @@
 Goal "A <= insert x B ==> A <= B & x ~: A | (? B'. A = insert x B' & B' <= B)";
 by (case_tac "x:A" 1);
 by  (Fast_tac 2);
-br  disjI2 1;
+by (rtac disjI2 1);
 by (res_inst_tac [("x","A-{x}")] exI 1);
 by (Fast_tac 1);
 qed "subset_insertD";