1.1 --- a/src/Pure/codegen.ML	Tue Jan 17 10:26:50 2006 +0100
     1.2 +++ b/src/Pure/codegen.ML	Tue Jan 17 16:36:57 2006 +0100
     1.3 @@ -81,7 +81,7 @@
     1.4    val quotes_of: 'a mixfix list -> 'a list
     1.5    val num_args_of: 'a mixfix list -> int
     1.6    val replace_quotes: 'b list -> 'a mixfix list -> 'b mixfix list
     1.7 -  val fillin_mixfix: 'a mixfix list -> Pretty.T list -> ('a -> Pretty.T) -> Pretty.T
     1.8 +  val fillin_mixfix: ('a -> Pretty.T) -> 'a mixfix list -> 'a list -> Pretty.T
     1.9    val mk_deftab: theory -> deftab
    1.10  
    1.11    val get_node: codegr -> string -> node
    1.12 @@ -658,12 +658,12 @@
    1.13    | replace_quotes (x::xs) (Quote _ :: ms) =
    1.14        Quote x :: replace_quotes xs ms;
    1.15  
    1.16 -fun fillin_mixfix ms args f =
    1.17 +fun fillin_mixfix f ms args =
    1.18    let
    1.19      fun fillin [] [] =
    1.20           []
    1.21        | fillin (Arg :: ms) (a :: args) =
    1.22 -          a :: fillin ms args
    1.23 +          f a :: fillin ms args
    1.24        | fillin (Ignore :: ms) args =
    1.25            fillin ms args
    1.26        | fillin (Module :: ms) args =
    1.27 @@ -671,7 +671,7 @@
    1.28        | fillin (Pretty p :: ms) args =
    1.29            p :: fillin ms args
    1.30        | fillin (Quote q :: ms) args =
    1.31 -          (f q) :: fillin ms args
    1.32 +          f q :: fillin ms args
    1.33    in Pretty.block (fillin ms args) end;
    1.34  
    1.35