1.1 --- a/doc-src/more_antiquote.ML Wed Jan 13 12:20:37 2010 +0100
1.2 +++ b/doc-src/more_antiquote.ML Thu Jan 14 09:18:08 2010 +0100
1.3 @@ -88,10 +88,12 @@
1.4 let
1.5 val thy = ProofContext.theory_of ctxt;
1.6 val const = Code.check_const thy raw_const;
1.7 - val (_, funcgr) = Code_Preproc.obtain thy [const] [];
1.8 + val (_, eqngr) = Code_Preproc.obtain thy [const] [];
1.9 fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
1.10 - val thms = Code_Preproc.eqns funcgr const
1.11 - |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
1.12 + val thms = Code_Preproc.cert eqngr const
1.13 + |> Code.equations_thms_cert thy
1.14 + |> snd
1.15 + |> map_filter (fn (_, (thm, proper)) => if proper then SOME thm else NONE)
1.16 |> map (holize o no_vars ctxt o AxClass.overload thy);
1.17 in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end;
1.18