doc-src/more_antiquote.ML
changeset 38917 c7da3cc88135
parent 38767 d8da44a8dd25
child 38921 15f8cffdbf5d
--- a/doc-src/more_antiquote.ML	Mon Aug 30 16:33:06 2010 +0200
+++ b/doc-src/more_antiquote.ML	Mon Aug 30 16:42:54 2010 +0200
@@ -130,6 +130,7 @@
       Code_Target.code_of thy
         target NONE "Example" (mk_cs thy)
         (fn naming => maps (fn f => f thy naming) mk_stmtss)
+      |> fst
       |> typewriter
     end);