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