# HG changeset patch
# User paulson
# Date 875526573 -7200
# Node ID c6abd2c3373fc52bb2198a1100d09bee357d3d18
# Parent  71366483323bef41b38a768ea25844a335a3eecc
Now using qed_spec_mp

diff -r 71366483323b -r c6abd2c3373f src/ZF/ex/Mutil.ML
--- 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);