1.1 --- a/doc-src/more_antiquote.ML	Fri Feb 19 22:37:43 2010 +0100
     1.2 +++ b/doc-src/more_antiquote.ML	Sat Feb 20 07:52:06 2010 +0100
     1.3 @@ -91,9 +91,9 @@
     1.4      val (_, eqngr) = Code_Preproc.obtain thy [const] [];
     1.5      fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
     1.6      val thms = Code_Preproc.cert eqngr const
     1.7 -      |> Code.equations_thms_cert thy
     1.8 +      |> Code.equations_of_cert thy
     1.9        |> snd
    1.10 -      |> map_filter (fn (_, (thm, proper)) => if proper then SOME thm else NONE)
    1.11 +      |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
    1.12        |> map (holize o no_vars ctxt o AxClass.overload thy);
    1.13    in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end;
    1.14