# HG changeset patch
# User wenzelm
# Date 967924318 -7200
# Node ID 64b7f756c8f04377914872a0e6c179f730ca7893
# Parent  98bb27b84363ff0faf338c314c7a0a32241080f5
"split": added "(asm)" option;

diff -r 98bb27b84363 -r 64b7f756c8f0 src/Provers/splitter.ML
--- 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;