# HG changeset patch
# User paulson
# Date 881142573 -3600
# Node ID 1983e4054fd8a4ec2b8e3710adb4ea52d6dc0b68
# Parent  50403e5a44c058d1006e7b62ac32f8550c3708c1
updated for latest Blast_tac, which treats equality differently

diff -r 50403e5a44c0 -r 1983e4054fd8 src/HOL/WF.ML
--- a/src/HOL/WF.ML	Wed Dec 03 10:48:16 1997 +0100
+++ b/src/HOL/WF.ML	Wed Dec 03 10:49:33 1997 +0100
@@ -108,8 +108,8 @@
 
 goal WF.thy "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)";
 by (rtac iffI 1);
- by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl] addIs
-      [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1);
+ by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl] 
+	addIs [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1);
 by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1);
 by Safe_tac;
 by (EVERY1[rtac allE, atac, etac impE, Blast_tac]);
@@ -124,7 +124,8 @@
 by (res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")] allE 1);
  by (assume_tac 1);
 by (thin_tac "! Q. (? x. x : Q) --> ?P Q" 1);	(*essential for speed*)
-by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
+(*Blast_tac with new substOccur fails*)
+by (best_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
 qed "wf_insert";
 AddIffs [wf_insert];