1.1 --- a/doc-src/more_antiquote.ML	Tue Feb 10 17:53:51 2009 -0800
     1.2 +++ b/doc-src/more_antiquote.ML	Wed Feb 11 15:05:25 2009 +0100
     1.3 @@ -93,9 +93,10 @@
     1.4      val thy = ProofContext.theory_of ctxt;
     1.5      val const = Code_Unit.check_const thy raw_const;
     1.6      val (_, funcgr) = Code_Funcgr.make thy [const];
     1.7 +    fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
     1.8      val thms = Code_Funcgr.eqns funcgr const
     1.9        |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    1.10 -      |> map (no_vars ctxt o AxClass.overload thy);
    1.11 +      |> map (holize o no_vars ctxt o AxClass.overload thy);
    1.12    in ThyOutput.output_list pretty_thm src ctxt thms end;
    1.13  
    1.14  in