| changeset 8168 | 9d2ac5439089 |
| parent 8154 | dab09e1ad594 |
| child 8170 | 4b9451fae406 |
--- a/src/Provers/simplifier.ML Fri Jan 28 21:56:55 2000 +0100 +++ b/src/Provers/simplifier.ML Fri Jan 28 21:57:15 2000 +0100 @@ -487,7 +487,7 @@ fun simp_method tac = (fn prems => fn ctxt => Method.METHOD (fn facts => - FINDGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt)))) + HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt)))) |> Method.bang_sectioned_args simp_modifiers';