# HG changeset patch
# User haftmann
# Date 1263457088 -3600
# Node ID a22b09addd78c28970a19049bfa883b017997a1d
# Parent  19fd499cddff39affb8f42abb7c05fdae46dfde0
adjusted to changes in code equation administration

diff -r 19fd499cddff -r a22b09addd78 doc-src/more_antiquote.ML
--- a/doc-src/more_antiquote.ML	Wed Jan 13 12:20:37 2010 +0100
+++ b/doc-src/more_antiquote.ML	Thu Jan 14 09:18:08 2010 +0100
@@ -88,10 +88,12 @@
   let
     val thy = ProofContext.theory_of ctxt;
     val const = Code.check_const thy raw_const;
-    val (_, funcgr) = Code_Preproc.obtain thy [const] [];
+    val (_, eqngr) = Code_Preproc.obtain thy [const] [];
     fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
-    val thms = Code_Preproc.eqns funcgr const
-      |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
+    val thms = Code_Preproc.cert eqngr const
+      |> Code.equations_thms_cert thy
+      |> snd
+      |> map_filter (fn (_, (thm, proper)) => if proper then SOME thm else NONE)
       |> map (holize o no_vars ctxt o AxClass.overload thy);
   in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end;