| changeset 18988 | d6e5fa2ba8b8 |
| parent 18728 | 6790126ab5f6 |
| child 20217 | 25b068a99d2b |
--- a/src/Provers/splitter.ML Fri Feb 10 02:22:13 2006 +0100 +++ b/src/Provers/splitter.ML Fri Feb 10 02:22:16 2006 +0100 @@ -448,7 +448,7 @@ Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)]; fun split_meth src = - Method.syntax Attrib.local_thms src + Method.syntax Attrib.thms src #> (fn (_, ths) => Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o gen_split_tac ths));