simplified 'split_format' syntax;

--- a/src/HOL/MicroJava/J/Eval.thy	Fri Feb 02 23:59:30 2001 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy	Sat Feb 03 00:01:54 2001 +0100
@@ -139,7 +139,7 @@
 	    G\<turnstile>s1 -c-> s2; G\<turnstile>s2 -While(e) c-> s3 |] ==>
          G\<turnstile>Norm s0 -While(e) c-> s3"
 
-lemmas eval_evals_exec_induct = eval_evals_exec.induct [complete_split]
+lemmas eval_evals_exec_induct = eval_evals_exec.induct [split_format (complete)]
 
 lemma NewCI: "[|new_Addr (heap s) = (a,x);  
        s' = c_hupd (heap s(a\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==>  

--- a/src/HOL/Tools/split_rule.ML	Fri Feb 02 23:59:30 2001 +0100
+++ b/src/HOL/Tools/split_rule.ML	Sat Feb 03 00:01:54 2001 +0100
@@ -127,26 +127,15 @@
 
 (* attribute syntax *)
 
-fun complete_split x =
-  Attrib.no_args (Drule.rule_attribute (K complete_split_rule)) x;
-
-fun split_format x =
-  Attrib.syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name))
-    >> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x;
-
-val split_attributes =
- [("complete_split", (complete_split, complete_split),
-    "recursively split all pair-typed function arguments"),
-  ("split_format", (split_format, split_format),
-    "split given pair-typed subterms in premises")];
-
-
-
-(** theory setup **)
+fun split_format x = Attrib.syntax
+  (Args.mode "complete" >> K (Drule.rule_attribute (K complete_split_rule)) ||
+    Args.and_list1 (Scan.lift (Scan.repeat Args.name))
+      >> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x;
 
 val setup =
- [Attrib.add_attributes split_attributes];
-
+ [Attrib.add_attributes
+  [("split_format", (split_format, split_format),
+    "split pair-typed subterms in premises, or function arguments")]];
 
 end;