tuned, including signature

--- a/src/Tools/Code/code_printer.ML	Sat May 18 13:04:10 2013 +0200
+++ b/src/Tools/Code/code_printer.ML	Sun May 19 20:15:00 2013 +0200
@@ -73,8 +73,8 @@
   datatype activated_const_syntax = Plain_const_syntax of int * string
     | Complex_const_syntax of activated_complex_const_syntax
   val requires_args: const_syntax -> int
-  val parse_const_syntax: Token.T list -> const_syntax option * Token.T list
-  val parse_tyco_syntax: Token.T list -> tyco_syntax option * Token.T list
+  val parse_const_syntax: Token.T list -> const_syntax * Token.T list
+  val parse_tyco_syntax: Token.T list -> tyco_syntax * Token.T list
   val plain_const_syntax: string -> const_syntax
   val simple_const_syntax: simple_const_syntax -> const_syntax
   val complex_const_syntax: complex_const_syntax -> const_syntax
@@ -387,13 +387,12 @@
   end;
 
 fun parse_syntax mk_plain mk_complex prep_arg =
-  Scan.option (
-      ((@{keyword "infix"} >> K X)
-        || (@{keyword "infixl"} >> K L)
-        || (@{keyword "infixr"} >> K R))
-        -- Parse.nat -- Parse.string
-        >> (fn ((x, i), s) => mk_complex (parse_infix prep_arg (x, i) s))
-      || Parse.string >> (fn s => (parse_mixfix mk_plain mk_complex prep_arg s)));
+  ((@{keyword "infix"} >> K X)
+    || (@{keyword "infixl"} >> K L)
+    || (@{keyword "infixr"} >> K R))
+    -- Parse.nat -- Parse.string
+    >> (fn ((x, i), s) => mk_complex (parse_infix prep_arg (x, i) s))
+  || Parse.string >> (fn s => (parse_mixfix mk_plain mk_complex prep_arg s));
 
 fun parse_tyco_syntax x = parse_syntax (fn s => (0, (K o K o K o str) s)) I I x;
 

--- a/src/Tools/Code/code_target.ML	Sat May 18 13:04:10 2013 +0200
+++ b/src/Tools/Code/code_target.ML	Sun May 19 20:15:00 2013 +0200
@@ -647,7 +647,7 @@
 fun process_multi_syntax parse_thing parse_syntax change =
   (Parse.and_list1 parse_thing
   :|-- (fn things => Scan.repeat1 (@{keyword "("} |-- Parse.name --
-        (zip_list things parse_syntax @{keyword "and"}) --| @{keyword ")"})))
+        (zip_list things (Scan.option parse_syntax) @{keyword "and"}) --| @{keyword ")"})))
   >> (Toplevel.theory oo fold)
     (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns);
 
@@ -689,24 +689,21 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "code_class"} "define code syntax for class"
-    (process_multi_syntax Parse.xname (Scan.option Parse.string)
+    (process_multi_syntax Parse.xname Parse.string
       add_class_syntax_cmd);
 
 val _ =
   Outer_Syntax.command @{command_spec "code_instance"} "define code syntax for instance"
-    (process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname)
-      (Scan.option (Parse.minus >> K ()))
+    (process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname) (Parse.minus >> K ())
       add_instance_syntax_cmd);
 
 val _ =
   Outer_Syntax.command @{command_spec "code_type"} "define code syntax for type constructor"
-    (process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
-      add_tyco_syntax_cmd);
+    (process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax add_tyco_syntax_cmd);
 
 val _ =
   Outer_Syntax.command @{command_spec "code_const"} "define code syntax for constant"
-    (process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
-      add_const_syntax_cmd);
+    (process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax add_const_syntax_cmd);
 
 val _ =
   Outer_Syntax.command @{command_spec "code_reserved"}