distinguish different classes of const syntax

--- a/src/HOL/Tools/list_code.ML	Mon Jul 19 11:55:43 2010 +0200
+++ b/src/HOL/Tools/list_code.ML	Mon Jul 19 11:55:44 2010 +0200
@@ -46,8 +46,8 @@
             Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
         | NONE =>
             default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
-  in Code_Target.add_syntax_const target
-    @{const_name Cons} (SOME (2, ([@{const_name Nil}, @{const_name Cons}], pretty)))
+  in Code_Target.add_syntax_const target @{const_name Cons}
+    (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
   end
 
 end;

--- a/src/HOL/Tools/numeral.ML	Mon Jul 19 11:55:43 2010 +0200
+++ b/src/HOL/Tools/numeral.ML	Mon Jul 19 11:55:44 2010 +0200
@@ -77,8 +77,8 @@
       (Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
   in
     thy |> Code_Target.add_syntax_const target number_of
-      (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
-        @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
+      (SOME (Code_Printer.complex_const_syntax (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
+        @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty))))
   end;
 
 end; (*local*)

--- a/src/HOL/Tools/string_code.ML	Mon Jul 19 11:55:43 2010 +0200
+++ b/src/HOL/Tools/string_code.ML	Mon Jul 19 11:55:44 2010 +0200
@@ -60,7 +60,7 @@
         | NONE =>
             List_Code.default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
   in Code_Target.add_syntax_const target
-    @{const_name Cons} (SOME (2, (cs_summa, pretty)))
+    @{const_name Cons} (SOME (Code_Printer.complex_const_syntax (2, (cs_summa, pretty))))
   end;
 
 fun add_literal_char target =
@@ -70,7 +70,7 @@
        of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
         | NONE => Code_Printer.eqn_error thm "Illegal character expression";
   in Code_Target.add_syntax_const target
-    @{const_name Char} (SOME (2, (cs_nibbles, pretty)))
+    @{const_name Char} (SOME (Code_Printer.complex_const_syntax (2, (cs_nibbles, pretty))))
   end;
 
 fun add_literal_string target =
@@ -83,7 +83,7 @@
               | NONE => Code_Printer.eqn_error thm "Illegal message expression")
         | NONE => Code_Printer.eqn_error thm "Illegal message expression";
   in Code_Target.add_syntax_const target 
-    @{const_name STR} (SOME (1, (cs_summa, pretty)))
+    @{const_name STR} (SOME (Code_Printer.complex_const_syntax (1, (cs_summa, pretty))))
   end;
 
 end;

--- a/src/Tools/Code/code_haskell.ML	Mon Jul 19 11:55:43 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Mon Jul 19 11:55:44 2010 +0200
@@ -218,30 +218,35 @@
       | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
           let
             val tyvars = intro_vars (map fst vs) reserved;
-            fun print_classparam_instance ((classparam, const), (thm, _)) = case syntax_const classparam
-             of NONE => semicolon [
-                    (str o deresolve_base) classparam,
-                    str "=",
-                    print_app tyvars (SOME thm) reserved NOBR (const, [])
-                  ]
-              | SOME (k, pr) =>
-                  let
-                    val (c, (_, tys)) = const;
-                    val (vs, rhs) = (apfst o map) fst
-                      (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
-                    val s = if (is_some o syntax_const) c
-                      then NONE else (SOME o Long_Name.base_name o deresolve) c;
-                    val vars = reserved
-                      |> intro_vars (map_filter I (s :: vs));
-                    val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
-                      (*dictionaries are not relevant at this late stage*)
-                  in
-                    semicolon [
-                      print_term tyvars (SOME thm) vars NOBR lhs,
+            fun requires_args classparam = case syntax_const classparam
+             of NONE => 0
+              | SOME (Code_Printer.Plain_const_syntax _) => 0
+              | SOME (Code_Printer.Complex_const_syntax (k,_ )) => k;
+            fun print_classparam_instance ((classparam, const), (thm, _)) =
+              case requires_args classparam
+               of 0 => semicolon [
+                      (str o deresolve_base) classparam,
                       str "=",
-                      print_term tyvars (SOME thm) vars NOBR rhs
+                      print_app tyvars (SOME thm) reserved NOBR (const, [])
                     ]
-                  end;
+                | k =>
+                    let
+                      val (c, (_, tys)) = const;
+                      val (vs, rhs) = (apfst o map) fst
+                        (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
+                      val s = if (is_some o syntax_const) c
+                        then NONE else (SOME o Long_Name.base_name o deresolve) c;
+                      val vars = reserved
+                        |> intro_vars (map_filter I (s :: vs));
+                      val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
+                        (*dictionaries are not relevant at this late stage*)
+                    in
+                      semicolon [
+                        print_term tyvars (SOME thm) vars NOBR lhs,
+                        str "=",
+                        print_term tyvars (SOME thm) vars NOBR rhs
+                      ]
+                    end;
           in
             Pretty.block_enclose (
               Pretty.block [
@@ -459,7 +464,7 @@
   in if target = target' then
     thy
     |> Code_Target.add_syntax_const target c_bind
-        (SOME (pretty_haskell_monad c_bind))
+        (SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))
   else error "Only Haskell target allows for monad syntax" end;
 
 

--- a/src/Tools/Code/code_printer.ML	Mon Jul 19 11:55:43 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Mon Jul 19 11:55:44 2010 +0200
@@ -67,17 +67,19 @@
 
   type tyco_syntax
   type simple_const_syntax
+  type complex_const_syntax
   type const_syntax
-  type activated_const_syntax
-  val parse_infix: ('a -> 'b) -> lrx * int -> string
-    -> int * ((fixity -> 'b -> Pretty.T)
-    -> fixity -> 'a list -> Pretty.T)
-  val parse_syntax: ('a -> 'b) -> Token.T list
-    -> (int * ((fixity -> 'b -> Pretty.T)
-    -> fixity -> 'a list -> Pretty.T)) option * Token.T list
+  type activated_complex_const_syntax
+  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 plain_const_syntax: string -> const_syntax
   val simple_const_syntax: simple_const_syntax -> const_syntax
+  val complex_const_syntax: complex_const_syntax -> const_syntax
   val activate_const_syntax: theory -> literals
-    -> const_syntax -> Code_Thingol.naming -> activated_const_syntax * Code_Thingol.naming
+    -> string -> const_syntax -> Code_Thingol.naming -> activated_const_syntax * Code_Thingol.naming
   val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
     -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> (string -> activated_const_syntax option)
@@ -243,31 +245,45 @@
 
 type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
   -> fixity -> (iterm * itype) list -> Pretty.T);
-type const_syntax = int * (string list * (literals -> string list
+
+type complex_const_syntax = int * (string list * (literals -> string list
   -> (var_ctxt -> fixity -> iterm -> Pretty.T)
     -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
-type activated_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
-  -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
+
+datatype const_syntax = plain_const_syntax of string
+  | complex_const_syntax of complex_const_syntax;
+
+fun requires_args (plain_const_syntax _) = 0
+  | requires_args (complex_const_syntax (k, _)) = k;
 
 fun simple_const_syntax syn =
-  apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn;
+  complex_const_syntax (apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn);
 
-fun activate_const_syntax thy literals (n, (cs, f)) naming =
-  fold_map (Code_Thingol.ensure_declared_const thy) cs naming
-  |-> (fn cs' => pair (n, f literals cs'));
+type activated_complex_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
+  -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)
+
+datatype activated_const_syntax = Plain_const_syntax of int * string
+  | Complex_const_syntax of activated_complex_const_syntax;
 
-fun gen_print_app print_app_expr print_term syntax_const thm vars fxy (app as ((c, (_, function_typs)), ts)) =
+fun activate_const_syntax thy literals c (plain_const_syntax s) naming =
+      (Plain_const_syntax (Code.args_number thy c, s), naming)
+  | activate_const_syntax thy literals c (complex_const_syntax (n, (cs, f))) naming =
+      fold_map (Code_Thingol.ensure_declared_const thy) cs naming
+      |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
+
+fun gen_print_app print_app_expr print_term syntax_const some_thm vars fxy (app as ((c, (_, function_typs)), ts)) =
   case syntax_const c
-   of NONE => brackify fxy (print_app_expr thm vars app)
-    | SOME (k, print) =>
+   of NONE => brackify fxy (print_app_expr some_thm vars app)
+    | SOME (Plain_const_syntax (_, s)) => brackify fxy (str s :: map (print_term some_thm vars BR) ts)
+    | SOME (Complex_const_syntax (k, print)) =>
         let
-          fun print' fxy ts = print (print_term thm) thm vars fxy (ts ~~ take k function_typs);
+          fun print' fxy ts = print (print_term some_thm) some_thm vars fxy (ts ~~ take k function_typs);
         in if k = length ts
           then print' fxy ts
         else if k < length ts
           then case chop k ts of (ts1, ts2) =>
-            brackify fxy (print' APP ts1 :: map (print_term thm vars BR) ts2)
-          else print_term thm vars fxy (Code_Thingol.eta_expand k app)
+            brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
+          else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
         end;
 
 fun gen_print_bind print_term thm (fxy : fixity) pat vars =
@@ -281,7 +297,8 @@
 
 datatype 'a mixfix =
     Arg of fixity
-  | Pretty of Pretty.T;
+  | String of string
+  | Break;
 
 fun mk_mixfix prep_arg (fixity_this, mfx) =
   let
@@ -292,8 +309,10 @@
           []
       | fillin print (Arg fxy :: mfx) (a :: args) =
           (print fxy o prep_arg) a :: fillin print mfx args
-      | fillin print (Pretty p :: mfx) args =
-          p :: fillin print mfx args;
+      | fillin print (String s :: mfx) args =
+          str s :: fillin print mfx args
+      | fillin print (Break :: mfx) args =
+          Pretty.brk 1 :: fillin print mfx args;
   in
     (i, fn print => fn fixity_ctxt => fn args =>
       gen_brackify (fixity fixity_this fixity_ctxt) (fillin print mfx args))
@@ -304,42 +323,45 @@
     val l = case x of L => INFX (i, L) | _ => INFX (i, X);
     val r = case x of R => INFX (i, R) | _ => INFX (i, X);
   in
-    mk_mixfix prep_arg (INFX (i, x),
-      [Arg l, (Pretty o str) " ", (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
+    mk_mixfix prep_arg (INFX (i, x), [Arg l, String " ", String s, Break, Arg r])
   end;
 
-fun parse_mixfix prep_arg s =
+fun parse_mixfix mk_plain mk_complex prep_arg s =
   let
     val sym_any = Scan.one Symbol.is_regular;
     val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (
          ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
       || ($$ "_" >> K (Arg BR))
-      || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
+      || ($$ "/" |-- Scan.repeat ($$ " ") >> (K Break))
       || (Scan.repeat1
            (   $$ "'" |-- sym_any
             || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
-                 sym_any) >> (Pretty o str o implode)));
+                 sym_any) >> (String o implode)));
   in case Scan.finite Symbol.stopper parse (Symbol.explode s)
-   of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p)
-    | ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p)
+   of ((false, [String s]), []) => mk_plain s
+    | ((_, p as [_]), []) => mk_complex (mk_mixfix prep_arg (NOBR, p))
+    | ((b, p as _ :: _ :: _), []) => mk_complex (mk_mixfix prep_arg (if b then NOBR else BR, p))
     | _ => Scan.!!
         (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
   end;
 
 val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
 
-fun parse_syntax prep_arg xs =
-  Scan.option ((
+fun parse_syntax mk_plain mk_complex prep_arg =
+  Scan.option (
       ((Parse.$$$ infixK >> K X)
         || (Parse.$$$ infixlK >> K L)
         || (Parse.$$$ infixrK >> K R))
-        -- Parse.nat >> parse_infix prep_arg
-      || Scan.succeed (parse_mixfix prep_arg))
-      -- Parse.string
-      >> (fn (parse, s) => parse s)) xs;
+        -- 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)));
 
 val _ = List.app Keyword.keyword [infixK, infixlK, infixrK];
 
+val parse_tyco_syntax = parse_syntax (fn s => (0, (K o K o K o str) s)) I I;
+
+val parse_const_syntax = parse_syntax plain_const_syntax simple_const_syntax fst;
+
 
 (** module name spaces **)
 

--- a/src/Tools/Code/code_scala.ML	Mon Jul 19 11:55:43 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Mon Jul 19 11:55:44 2010 +0200
@@ -76,17 +76,20 @@
         (app as ((c, ((arg_typs, _), function_typs)), ts)) =
       let
         val k = length ts;
-        val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
         val arg_typs' = if is_pat orelse
           (is_none (syntax_const c) andalso is_singleton_constr c) then [] else arg_typs;
-        val (no_syntax, print') = case syntax_const c
-         of NONE => (true, fn ts => applify "(" ")"
+        val (l, print') = case syntax_const c
+         of NONE => (args_num c, fn ts => applify "(" ")"
               (print_term tyvars is_pat some_thm vars NOBR) fxy
                 (applify "[" "]" (print_typ tyvars NOBR)
                   NOBR ((str o deresolve) c) arg_typs') ts)
-          | SOME (_, print) => (false, fn ts =>
-              print (print_term tyvars is_pat some_thm) some_thm vars fxy
-                (ts ~~ take l function_typs));
+          | SOME (Plain_const_syntax (k, s)) => (k, fn ts => applify "(" ")"
+              (print_term tyvars is_pat some_thm vars NOBR) fxy
+                (applify "[" "]" (print_typ tyvars NOBR)
+                  NOBR (str s) arg_typs') ts)
+          | SOME (Complex_const_syntax (k, print)) =>
+              (k, fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
+                (ts ~~ take k function_typs))
       in if k = l then print' ts
       else if k < l then
         print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
@@ -355,20 +358,22 @@
       | _ => false;
     val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
       reserved args_num is_singleton_constr deresolver;
-    fun print_module name content =
-      (name, Pretty.chunks [
-        str ("object " ^ name ^ " {"),
-        str "",
+    fun print_module name imports content =
+      (name, Pretty.chunks (
+        str ("object " ^ name ^ " {")
+        :: (if null imports then []
+          else str "" :: map (fn name => str ("import " ^ name ^ "._")) imports)
+        @ [str "",
         content,
         str "",
-        str "}"
-      ]);
+        str "}"]
+      ));
     fun serialize_module the_module_name sca_program =
       let
         val content = Pretty.chunks2 (map_filter
           (fn (name, (_, SOME stmt)) => SOME (print_stmt (name, stmt))
             | (_, (_, NONE)) => NONE) sca_program);
-      in print_module the_module_name content end;
+      in print_module the_module_name (map fst includes) content end;
     fun check_destination destination =
       (File.check destination; destination);
     fun write_module destination (modlname, content) =
@@ -385,7 +390,7 @@
       (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
         (write_module (check_destination file)))
       (rpair [] o cat_lines o map (code_of_pretty o snd))
-      (map (uncurry print_module) includes
+      (map (fn (name, content) => print_module name [] content) includes
         @| serialize_module the_module_name sca_program)
       destination
   end;
@@ -405,7 +410,7 @@
   literal_char = Library.enclose "'" "'" o char_scala,
   literal_string = quote o translate_string char_scala,
   literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
-  literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
+  literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
   literal_naive_numeral = fn k => if k >= 0
     then string_of_int k else "(- " ^ string_of_int (~ k) ^ ")",
   literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],

--- a/src/Tools/Code/code_target.ML	Mon Jul 19 11:55:43 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Mon Jul 19 11:55:44 2010 +0200
@@ -244,11 +244,11 @@
   |>> map_filter I;
 
 fun activate_const_syntax thy literals src_tab naming = (Symtab.empty, naming)
-  |> fold_map (fn thing_identifier => fn (tab, naming) =>
-      case Code_Thingol.lookup_const naming thing_identifier
+  |> fold_map (fn c => fn (tab, naming) =>
+      case Code_Thingol.lookup_const naming c
        of SOME name => let
               val (syn, naming') = Code_Printer.activate_const_syntax thy
-                literals (the (Symtab.lookup src_tab thing_identifier)) naming
+                literals c (the (Symtab.lookup src_tab c)) naming
             in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end
         | NONE => (NONE, (tab, naming))) (Symtab.keys src_tab)
   |>> map_filter I;
@@ -445,12 +445,12 @@
       then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
       else syn);
 
-fun gen_add_syntax_const prep_const prep_syn =
+fun gen_add_syntax_const prep_const =
   gen_add_syntax (apsnd o apsnd, Symtab.update, Symtab.delete_safe) prep_const
-    (fn thy => fn c => fn raw_syn => let val syn = prep_syn raw_syn in
-      if fst syn > Code.args_number thy c
+    (fn thy => fn c => fn syn =>
+      if Code_Printer.requires_args syn > Code.args_number thy c
       then error ("Too many arguments in syntax for constant " ^ quote c)
-      else syn end);
+      else syn);
 
 fun add_reserved target =
   let
@@ -496,22 +496,23 @@
 
 fun zip_list (x::xs) f g =
   f
-  #-> (fn y =>
+  :|-- (fn y =>
     fold_map (fn x => g |-- f >> pair x) xs
-    #-> (fn xys => pair ((x, y) :: xys)));
+    :|-- (fn xys => pair ((x, y) :: xys)));
 
-fun parse_multi_syntax parse_thing parse_syntax =
-  Parse.and_list1 parse_thing
-  #-> (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name --
-        (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")"));
+fun process_multi_syntax parse_thing parse_syntax change =
+  (Parse.and_list1 parse_thing
+  :|-- (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name --
+        (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")")))
+  >> (Toplevel.theory oo fold)
+    (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns);
 
 in
 
 val add_syntax_class = gen_add_syntax_class cert_class;
 val add_syntax_inst = gen_add_syntax_inst cert_inst;
 val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
-val add_syntax_const_simple = gen_add_syntax_const (K I) Code_Printer.simple_const_syntax;
-val add_syntax_const = gen_add_syntax_const (K I) I;
+val add_syntax_const = gen_add_syntax_const (K I);
 val allow_abort = gen_allow_abort (K I);
 val add_reserved = add_reserved;
 val add_include = add_include;
@@ -519,9 +520,7 @@
 val add_syntax_class_cmd = gen_add_syntax_class read_class;
 val add_syntax_inst_cmd = gen_add_syntax_inst read_inst;
 val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
-val add_syntax_const_simple_cmd = gen_add_syntax_const Code.read_const Code_Printer.simple_const_syntax;
-val add_syntax_const_cmd = gen_add_syntax_const Code.read_const I;
-
+val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
 val allow_abort_cmd = gen_allow_abort Code.read_const;
 
 fun parse_args f args =
@@ -550,32 +549,24 @@
 
 val _ =
   Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
-    parse_multi_syntax Parse.xname (Scan.option Parse.string)
-    >> (Toplevel.theory oo fold) (fn (target, syns) =>
-          fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
-  );
+    process_multi_syntax Parse.xname (Scan.option Parse.string)
+    add_syntax_class_cmd);
 
 val _ =
   Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
-    parse_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
+    process_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
       (Scan.option (Parse.minus >> K ()))
-    >> (Toplevel.theory oo fold) (fn (target, syns) =>
-          fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
-  );
+    add_syntax_inst_cmd);
 
 val _ =
   Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl (
-    parse_multi_syntax Parse.xname (Code_Printer.parse_syntax I)
-    >> (Toplevel.theory oo fold) (fn (target, syns) =>
-          fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
-  );
+    process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
+    add_syntax_tyco_cmd);
 
 val _ =
   Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl (
-    parse_multi_syntax Parse.term_group (Code_Printer.parse_syntax fst)
-    >> (Toplevel.theory oo fold) (fn (target, syns) =>
-      fold (fn (raw_const, syn) => add_syntax_const_simple_cmd target raw_const syn) syns)
-  );
+    process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
+    add_syntax_const_cmd);
 
 val _ =
   Outer_Syntax.command "code_reserved" "declare words as reserved for target language"