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))));