src/HOL/UNITY/Reach.ML

--- a/src/HOL/UNITY/Reach.ML	Wed Sep 23 10:03:32 1998 +0200
+++ b/src/HOL/UNITY/Reach.ML	Wed Sep 23 10:11:18 1998 +0200
@@ -113,7 +113,7 @@
 by (ensures_tac "asgt a b" 1);
 by (Blast_tac 2);
 by (full_simp_tac (simpset() addsimps [not_less_iff_le]) 1);
-bd (metric_le RS le_anti_sym) 1;
+by (dtac (metric_le RS le_anti_sym) 1);
 by (auto_tac (claset() addEs [less_not_refl3 RSN (2, rev_notE)],
 	      simpset()));
 qed "LeadsTo_Diff_fixedpoint";