--- a/src/Provers/splitter.ML Sat Sep 02 21:51:32 2000 +0200
+++ b/src/Provers/splitter.ML Sat Sep 02 21:51:58 2000 +0200
@@ -420,7 +420,10 @@
Args.$$$ splitN -- Args.$$$ "add" -- Args.colon >> K (I, split_add_local),
Args.$$$ splitN -- Args.$$$ "del" -- Args.colon >> K (I, split_del_local)];
-val split_meth = Method.thms_args (Method.SIMPLE_METHOD' HEADGOAL o split_tac);
+val split_args = #2 oo Method.syntax (Args.mode "asm" -- Attrib.local_thms);
+
+fun split_meth (asm, ths) =
+ Method.SIMPLE_METHOD' HEADGOAL (if asm then split_asm_tac ths else split_tac ths);
@@ -428,6 +431,6 @@
val setup =
[Attrib.add_attributes [(splitN, split_attr, "declare splitter rule")],
- Method.add_methods [(splitN, split_meth, "apply splitter rule")]];
+ Method.add_methods [(splitN, split_meth oo split_args, "apply splitter rule")]];
end;