1.1 --- a/src/Tools/code/code_target.ML	Wed Aug 06 00:12:26 2008 +0200
     1.2 +++ b/src/Tools/code/code_target.ML	Wed Aug 06 00:12:31 2008 +0200
     1.3 @@ -2239,7 +2239,7 @@
     1.4  val (inK, module_nameK, fileK) = ("in", "module_name", "file");
     1.5  
     1.6  fun code_exprP cmd =
     1.7 -  (Scan.repeat P.term
     1.8 +  (Scan.repeat P.term_group
     1.9    -- Scan.repeat (P.$$$ inK |-- P.name
    1.10       -- Scan.option (P.$$$ module_nameK |-- P.name)
    1.11       -- Scan.option (P.$$$ fileK |-- P.name)
    1.12 @@ -2252,7 +2252,7 @@
    1.13    OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
    1.14      parse_multi_syntax P.xname
    1.15        (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
    1.16 -        (P.term --| (P.$$$ "\<equiv>" || P.$$$ "==") -- P.string)) []))
    1.17 +        (P.term_group --| (P.$$$ "\<equiv>" || P.$$$ "==") -- P.string)) []))
    1.18      >> (Toplevel.theory oo fold) (fn (target, syns) =>
    1.19            fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
    1.20    );
    1.21 @@ -2274,14 +2274,14 @@
    1.22  
    1.23  val _ =
    1.24    OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl (
    1.25 -    parse_multi_syntax P.term (parse_syntax fst)
    1.26 +    parse_multi_syntax P.term_group (parse_syntax fst)
    1.27      >> (Toplevel.theory oo fold) (fn (target, syns) =>
    1.28            fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (simple_const_syntax syn)) syns)
    1.29    );
    1.30  
    1.31  val _ =
    1.32    OuterSyntax.command "code_monad" "define code syntax for monads" K.thy_decl (
    1.33 -    P.term -- P.term -- P.name
    1.34 +    P.term_group -- P.term_group -- P.name
    1.35      >> (fn ((raw_run, raw_bind), target) => Toplevel.theory 
    1.36            (add_monad target raw_run raw_bind))
    1.37    );
    1.38 @@ -2307,7 +2307,7 @@
    1.39  
    1.40  val _ =
    1.41    OuterSyntax.command "code_abort" "permit constant to be implemented as program abort" K.thy_decl (
    1.42 -    Scan.repeat1 P.term >> (Toplevel.theory o fold allow_abort_cmd)
    1.43 +    Scan.repeat1 P.term_group >> (Toplevel.theory o fold allow_abort_cmd)
    1.44    );
    1.45  
    1.46  val _ =