changeset 32283 | 3bebc195c124 |
parent 32282 | 853ef99c04cc |
child 33317 | b4534348b8fd |
--- a/src/CCL/Wfd.thy Thu Jul 30 11:23:57 2009 +0200 +++ b/src/CCL/Wfd.thy Thu Jul 30 12:20:43 2009 +0200 @@ -499,7 +499,7 @@ in fun eval_tac ths = - FOCUS_PREMS (fn {context, prems, ...} => + Subgoal.FOCUS_PREMS (fn {context, prems, ...} => DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get context) 1)); val eval_setup =