author | haftmann |
Fri, 11 Dec 2009 20:32:49 +0100 | |
changeset 34072 | 99eda1d59da9 |
parent 34071 | 93bfbb557e2e |
child 34073 | 7b0bf55adecd |
1.1 --- a/doc-src/more_antiquote.ML Fri Dec 11 20:32:49 2009 +0100 1.2 +++ b/doc-src/more_antiquote.ML Fri Dec 11 20:32:49 2009 +0100 1.3 @@ -126,7 +126,7 @@ 1.4 (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) => 1.5 let val thy = ProofContext.theory_of ctxt in 1.6 Code_Target.code_of thy 1.7 - target "Example" (mk_cs thy) 1.8 + target NONE "Example" (mk_cs thy) 1.9 (fn naming => maps (fn f => f thy naming) mk_stmtss) 1.10 |> typewriter 1.11 end);