
diff -r 16bc5564535f -r ff997038e8eb src/HOL/List.thy
--- 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"]




