diff -r fd6b9bdb428e -r 15f8cffdbf5d doc-src/more_antiquote.ML
--- a/doc-src/more_antiquote.ML	Mon Aug 30 18:32:40 2010 +0200
+++ b/doc-src/more_antiquote.ML	Tue Aug 31 13:08:58 2010 +0200
@@ -127,9 +127,9 @@
   (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
   (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) =>
     let val thy = ProofContext.theory_of ctxt in
-      Code_Target.code_of thy
-        target NONE "Example" (mk_cs thy)
+      Code_Target.produce_code thy (mk_cs thy)
         (fn naming => maps (fn f => f thy naming) mk_stmtss)
+        target NONE (SOME "Example") []
       |> fst
       |> typewriter
     end);