diff -r 00f8be1b7209 -r f87c8c449018 src/ZF/Coind/Map.ML
--- a/src/ZF/Coind/Map.ML	Thu Aug 24 00:55:42 2000 +0200
+++ b/src/ZF/Coind/Map.ML	Thu Aug 24 11:05:20 2000 +0200
@@ -4,8 +4,6 @@
     Copyright   1995  University of Cambridge
 *)
 
-open Map;
-
 (** Some sample proofs of inclusions for the final coalgebra "U" (by lcp) **)
 
 Goalw [TMap_def] "{0,1} <= {1} Un TMap(I, {0,1})";
@@ -20,7 +18,7 @@
 by (Blast_tac 1);
 result();
 
-(*TOO SLOW
+(*
 Goalw [TMap_def]
      "{0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2) <= \
 \     {1} Un TMap(I, {0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2))";
@@ -81,7 +79,7 @@
 (* ############################################################ *)
 
 Goalw [PMap_def,TMap_def] "B<=C ==> PMap(A,B)<=PMap(A,C)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "map_mono";
 
 (* Rename to pmap_mono *)