changeset 8476 | 07d3e6383822 |
parent 8468 | d99902232df8 |
child 8634 | 3f34637cb9c0 |
--- a/src/Provers/splitter.ML Wed Mar 15 18:50:48 2000 +0100 +++ b/src/Provers/splitter.ML Wed Mar 15 18:52:07 2000 +0100 @@ -422,7 +422,7 @@ (* method modifiers *) val split_modifiers = - [Args.$$$ splitN -- Args.$$$ ":" >> K (I, split_add_local), + [Args.$$$ splitN -- Args.$$$ ":" >> K ((I, split_add_local): Method.modifier), Args.$$$ splitN -- Args.$$$ addN -- Args.$$$ ":" >> K (I, split_add_local), Args.$$$ splitN -- Args.$$$ delN -- Args.$$$ ":" >> K (I, split_del_local)];