# HG changeset patch
# User nipkow
# Date 976696259 -3600
# Node ID e6a4bb832b46a876fc20812183b24757df365d7c
# Parent  bb3a81a005f75d6da247ba95b23fccaee7eeabff
sar split method uses new gen_split_tac.

diff -r bb3a81a005f7 -r e6a4bb832b46 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Tue Dec 12 14:08:48 2000 +0100
+++ b/src/Provers/splitter.ML	Wed Dec 13 09:30:59 2000 +0100
@@ -372,7 +372,12 @@
   in SUBGOAL tac
   end;
 
-
+fun gen_split_tac [] = K no_tac
+  | gen_split_tac (split::splits) =
+      let val (_,asm) = split_thm_info split
+      in (if asm then split_asm_tac else split_tac) [split] ORELSE'
+         gen_split_tac splits
+      end;
 
 (** declare split rules **)
 
@@ -420,10 +425,9 @@
   Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add_local),
   Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del_local)];
 
-val split_args = #2 oo Method.syntax (Args.mode "asm" -- Attrib.local_thms);
+val split_args = #2 oo Method.syntax Attrib.local_thms;
 
-fun split_meth (asm, ths) =
-  Method.SIMPLE_METHOD' HEADGOAL (if asm then split_asm_tac ths else split_tac ths);
+fun split_meth ths = Method.SIMPLE_METHOD' HEADGOAL (gen_split_tac ths);