--- a/src/Provers/splitter.ML Wed Mar 18 11:57:28 2009 +0100
+++ b/src/Provers/splitter.ML Wed Mar 18 15:23:52 2009 +0100
@@ -472,8 +472,8 @@
Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add),
Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)];
-val split_meth = Attrib.thms >>
- (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths)));
+fun split_meth parser = (Attrib.thms >>
+ (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths)))) parser;
(* theory setup *)