diff -r 4a1ee3043101 -r 60205b0de9b9 src/ZF/ex/BT.ML
--- a/src/ZF/ex/BT.ML	Mon Jul 13 16:42:27 1998 +0200
+++ b/src/ZF/ex/BT.ML	Mon Jul 13 16:43:57 1998 +0200
@@ -19,7 +19,7 @@
 
 (**  Lemmas to justify using "bt" in other recursive type definitions **)
 
-Goalw bt.defs "!!A B. A<=B ==> bt(A) <= bt(B)";
+Goalw bt.defs "A<=B ==> bt(A) <= bt(B)";
 by (rtac lfp_mono 1);
 by (REPEAT (rtac bt.bnd_mono 1));
 by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
@@ -110,7 +110,7 @@
 val [bt_reflect_Lf, bt_reflect_Br] = bt_recs bt_reflect_def;
 Addsimps [bt_reflect_Lf, bt_reflect_Br];
 
-Goalw [bt_reflect_def] "!!xs. xs: bt(A) ==> bt_reflect(xs) : bt(A)";
+Goalw [bt_reflect_def] "xs: bt(A) ==> bt_reflect(xs) : bt(A)";
 by (REPEAT (ares_tac (bt.intrs @ [bt_rec_type]) 1));
 qed "bt_reflect_type";