adjusted to changes in code equation administration
authorhaftmann
Thu Jan 14 09:18:08 2010 +0100 (2010-01-14)
changeset 34896a22b09addd78
parent 34895 19fd499cddff
child 34897 cf9e3426c7b1
child 34904 9c4d5db7c7ad
adjusted to changes in code equation administration
doc-src/more_antiquote.ML
     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