# HG changeset patch
# User wenzelm
# Date 953142727 -3600
# Node ID 07d3e6383822b62e0b84022f0624aed9a4649440
# Parent  deb604b3d9a9cc3b9eac0ed9b90313aed5c693d9
made SML/XL happy;

diff -r deb604b3d9a9 -r 07d3e6383822 src/Provers/splitter.ML
--- 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)];