| changeset 8671 | 6ce91a80f616 |
| parent 8667 | 4230d17073ea |
| child 8699 | f93e2dbab862 |
--- a/src/Provers/classical.ML Wed Apr 05 21:02:19 2000 +0200 +++ b/src/Provers/classical.ML Wed Apr 05 21:02:31 2000 +0200 @@ -1060,7 +1060,7 @@ (* METHOD_CLASET' *) fun METHOD_CLASET' tac ctxt = - Method.METHOD (FINDGOAL o tac (get_local_claset ctxt)); + Method.METHOD (HEADGOAL o tac (get_local_claset ctxt)); val trace_rules = ref false;