# HG changeset patch
# User haftmann
# Date 1131361571 -3600
# Node ID 7a524bfa8d65d285c6f6b1d750693a2339e15147
# Parent  60220e93528754e2c006b1511d3eaa050f7ca042
added proper fillin_mixfix

diff -r 60220e935287 -r 7a524bfa8d65 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Mon Nov 07 11:39:24 2005 +0100
+++ b/src/Pure/codegen.ML	Mon Nov 07 12:06:11 2005 +0100
@@ -80,7 +80,7 @@
   val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
   val quotes_of: 'a mixfix list -> 'a list
   val replace_quotes: 'b list -> 'a mixfix list -> 'b mixfix list
-  val fillin_mixfix: 'a mixfix list -> Pretty.T list -> Pretty.T list -> string list * Pretty.T
+  val fillin_mixfix: 'a mixfix list -> Pretty.T list -> ('a -> Pretty.T) -> string list * Pretty.T
   val mk_deftab: theory -> deftab
 
   val get_node: codegr -> string -> node
@@ -649,24 +649,24 @@
   | replace_quotes (x::xs) (Quote _ :: ms) =
       Quote x :: replace_quotes xs ms;
 
-fun fillin_mixfix ms args qs =
+fun fillin_mixfix ms args f =
   let
-    fun fillin [] [] [] vars = (vars, [])
-      | fillin (Arg :: ms) [] qs vars =
+    fun fillin [] [] vars = (vars, [])
+      | fillin (Arg :: ms) [] vars =
           let
             val v = "a_" ^ (string_of_int o length) vars;
-          in fillin ms args qs (v::vars) ||> (cons o Pretty.str) v end
-      | fillin (Arg :: ms) (a :: args) qs vars =
-          fillin ms args qs vars ||> cons a
-      | fillin (Ignore :: ms) args qs vars =
-          fillin ms args qs vars
-      | fillin (Module :: ms) args qs vars =
-          fillin ms args qs vars
-      | fillin (Pretty p :: ms) args qs vars =
-          fillin ms args qs vars ||> cons p
-      | fillin (Quote _ :: ms) args (q::qs) vars =
-          fillin ms args qs vars ||> cons q
-  in fillin ms args qs [] ||> Pretty.block end;
+          in fillin ms args (v::vars) ||> (cons o Pretty.str) v end
+      | fillin (Arg :: ms) (a :: args) vars =
+          fillin ms args vars ||> cons a
+      | fillin (Ignore :: ms) args vars =
+          fillin ms args vars
+      | fillin (Module :: ms) args vars =
+          fillin ms args vars
+      | fillin (Pretty p :: ms) args vars =
+          fillin ms args vars ||> cons p
+      | fillin (Quote q :: ms) args vars =
+          fillin ms args vars ||> cons (f q)
+  in fillin ms args [] ||> Pretty.block end;
 
 
 (**** default code generators ****)