Now using qed_spec_mp

--- a/src/ZF/ex/Mutil.ML	Mon Sep 29 11:48:48 1997 +0200
+++ b/src/ZF/ex/Mutil.ML	Mon Sep 29 11:49:33 1997 +0200
@@ -72,7 +72,7 @@
 by (asm_full_simp_tac (!simpset addsimps [Un_assoc,
 					  subset_empty_iff RS iff_sym]) 1);
 by (blast_tac (!claset addIs tiling.intrs) 1);
-bind_thm ("tiling_UnI", result() RS mp RS mp);
+qed_spec_mp "tiling_UnI";
 
 goal thy "!!t. t:tiling(domino) ==> Finite(t)";
 by (eresolve_tac [tiling.induct] 1);