| changeset 8154 | dab09e1ad594 |
| parent 7646 | 1ad3866b86cc |
| child 8168 | 9d2ac5439089 |
--- a/src/Provers/simplifier.ML Fri Jan 28 12:10:47 2000 +0100 +++ b/src/Provers/simplifier.ML Fri Jan 28 12:12:06 2000 +0100 @@ -487,7 +487,7 @@ fun simp_method tac = (fn prems => fn ctxt => Method.METHOD (fn facts => - FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt)))) + FINDGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt)))) |> Method.bang_sectioned_args simp_modifiers';