Deleted unused fillin_mixfix function.
authorberghofe
Wed Aug 29 10:20:22 2007 +0200 (2007-08-29)
changeset 2446901fd2863d7c8
parent 24468 15012073f0c1
child 24470 41c81e23c08d
Deleted unused fillin_mixfix function.
src/Pure/codegen.ML
     1.1 --- a/src/Pure/codegen.ML	Wed Aug 29 00:49:48 2007 +0200
     1.2 +++ b/src/Pure/codegen.ML	Wed Aug 29 10:20:22 2007 +0200
     1.3 @@ -82,7 +82,6 @@
     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 -> Pretty.T) -> 'a mixfix list -> 'a list -> Pretty.T
     1.8    val mk_deftab: theory -> deftab
     1.9    val add_unfold: thm -> theory -> theory
    1.10  
    1.11 @@ -624,22 +623,6 @@
    1.12    | replace_quotes (x::xs) (Quote _ :: ms) =
    1.13        Quote x :: replace_quotes xs ms;
    1.14  
    1.15 -fun fillin_mixfix f ms args =
    1.16 -  let
    1.17 -    fun fillin [] [] =
    1.18 -         []
    1.19 -      | fillin (Arg :: ms) (a :: args) =
    1.20 -          f a :: fillin ms args
    1.21 -      | fillin (Ignore :: ms) args =
    1.22 -          fillin ms args
    1.23 -      | fillin (Module :: ms) args =
    1.24 -          fillin ms args
    1.25 -      | fillin (Pretty p :: ms) args =
    1.26 -          p :: fillin ms args
    1.27 -      | fillin (Quote q :: ms) args =
    1.28 -          f q :: fillin ms args
    1.29 -  in Pretty.block (fillin ms args) end;
    1.30 -
    1.31  
    1.32  (**** default code generators ****)
    1.33