| changeset 49845 | 9b19c0e81166 |
| parent 42495 | 1af81b70cf09 |
| child 52223 | 5bb6ae8acb87 |
--- a/src/Pure/subgoal.ML Sat Oct 13 00:08:36 2012 +0200 +++ b/src/Pure/subgoal.ML Sat Oct 13 16:19:16 2012 +0200 @@ -140,7 +140,7 @@ val FOCUS_PREMS = GEN_FOCUS (true, false); val FOCUS = GEN_FOCUS (true, true); -fun SUBPROOF tac ctxt = FOCUS (Seq.map (tap (Goal.check_finished ctxt)) oo tac) ctxt; +fun SUBPROOF tac ctxt = FOCUS (Seq.map (Goal.check_finished ctxt) oo tac) ctxt; end;