src/Doc/more_antiquote.ML

--- a/src/Doc/more_antiquote.ML	Wed Jan 01 01:05:30 2014 +0100
+++ b/src/Doc/more_antiquote.ML	Wed Jan 01 01:05:46 2014 +0100
@@ -35,6 +35,7 @@
     val thms = Code_Preproc.cert eqngr const
       |> Code.equations_of_cert thy
       |> snd
+      |> these
       |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
       |> map (holize o no_vars ctxt o Axclass.overload thy);
   in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end;