doc-src/more_antiquote.ML
changeset 39147 15f8cffdbf5d
parent 39143 c7da3cc88135
child 39155 d9ac9dee764d
     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);