# HG changeset patch
# User berghofe
# Date 1188375622 -7200
# Node ID 01fd2863d7c8b2a4941d07c3d6a62a357810ed56
# Parent  15012073f0c1cc298f2aa53a7f70132c4f75cead
Deleted unused fillin_mixfix function.

diff -r 15012073f0c1 -r 01fd2863d7c8 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Wed Aug 29 00:49:48 2007 +0200
+++ b/src/Pure/codegen.ML	Wed Aug 29 10:20:22 2007 +0200
@@ -82,7 +82,6 @@
   val quotes_of: 'a mixfix list -> 'a list
   val num_args_of: 'a mixfix list -> int
   val replace_quotes: 'b list -> 'a mixfix list -> 'b mixfix list
-  val fillin_mixfix: ('a -> Pretty.T) -> 'a mixfix list -> 'a list -> Pretty.T
   val mk_deftab: theory -> deftab
   val add_unfold: thm -> theory -> theory
 
@@ -624,22 +623,6 @@
   | replace_quotes (x::xs) (Quote _ :: ms) =
       Quote x :: replace_quotes xs ms;
 
-fun fillin_mixfix f ms args =
-  let
-    fun fillin [] [] =
-         []
-      | fillin (Arg :: ms) (a :: args) =
-          f a :: fillin ms args
-      | fillin (Ignore :: ms) args =
-          fillin ms args
-      | fillin (Module :: ms) args =
-          fillin ms args
-      | fillin (Pretty p :: ms) args =
-          p :: fillin ms args
-      | fillin (Quote q :: ms) args =
-          f q :: fillin ms args
-  in Pretty.block (fillin ms args) end;
-
 
 (**** default code generators ****)