| changeset 10821 | dcb75538f542 |
| parent 10652 | e6a4bb832b46 |
| child 13157 | 4a4599f78f18 |
--- a/src/Provers/splitter.ML Sun Jan 07 21:40:49 2001 +0100 +++ b/src/Provers/splitter.ML Sun Jan 07 21:41:56 2001 +0100 @@ -427,7 +427,7 @@ val split_args = #2 oo Method.syntax Attrib.local_thms; -fun split_meth ths = Method.SIMPLE_METHOD' HEADGOAL (gen_split_tac ths); +fun split_meth ths = Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o gen_split_tac ths);