src/HOL/WF.ML
changeset 5521 7970832271cc
parent 5452 b38332431a8c
child 5579 32f99ca617b7
--- a/src/HOL/WF.ML	Mon Sep 21 23:06:37 1998 +0200
+++ b/src/HOL/WF.ML	Mon Sep 21 23:12:31 1998 +0200
@@ -177,7 +177,7 @@
   by (Blast_tac 1);
  by (blast_tac (claset() addEs [equalityE]) 1);
 by (Asm_full_simp_tac 1);
-by (Fast_tac 1);  (*faster than Blast_tac*)
+by (fast_tac (claset() delWrapper "bspec") 1); (*faster than Blast_tac*)
 qed "wf_UN";
 
 Goalw [Union_def]