src/CCL/Fix.ML
changeset 17955 3b34516662c6
parent 17456 bcf7544875b2
--- a/src/CCL/Fix.ML	Fri Oct 21 16:34:22 2005 +0200
+++ b/src/CCL/Fix.ML	Fri Oct 21 18:14:32 2005 +0200
@@ -182,7 +182,7 @@
 by (REPEAT_SOME (ares_tac [allI]));
 by (stac applyBbot 1);
 by (resolve_tac prems 1);
-br (applyB RS ssubst )1;
+by (rtac (applyB RS ssubst) 1);
 by (res_inst_tac [("t","xa")] term_case 1);
 by (ALLGOALS (simp_tac term_ss));
 by (ALLGOALS (fast_tac (term_cs addIs ([all_INCL,INCL_subst] @ prems))));