1.1 --- a/doc-src/more_antiquote.ML Mon Aug 30 18:32:40 2010 +0200
1.2 +++ b/doc-src/more_antiquote.ML Tue Aug 31 13:08:58 2010 +0200
1.3 @@ -127,9 +127,9 @@
1.4 (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
1.5 (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) =>
1.6 let val thy = ProofContext.theory_of ctxt in
1.7 - Code_Target.code_of thy
1.8 - target NONE "Example" (mk_cs thy)
1.9 + Code_Target.produce_code thy (mk_cs thy)
1.10 (fn naming => maps (fn f => f thy naming) mk_stmtss)
1.11 + target NONE (SOME "Example") []
1.12 |> fst
1.13 |> typewriter
1.14 end);