--- a/src/HOL/List.thy Tue Apr 19 22:32:49 2011 +0200
+++ b/src/HOL/List.thy Tue Apr 19 23:57:28 2011 +0200
@@ -5207,13 +5207,13 @@
setup {*
let
- fun list_codegen thy defs dep thyname b t gr =
+ fun list_codegen thy mode defs dep thyname b t gr =
let
val ts = HOLogic.dest_list t;
- val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
+ val (_, gr') = Codegen.invoke_tycodegen thy mode defs dep thyname false
(fastype_of t) gr;
val (ps, gr'') = fold_map
- (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
+ (Codegen.invoke_codegen thy mode defs dep thyname false) ts gr'
in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
in
fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"]