# HG changeset patch
# User haftmann
# Date 1234361125 -3600
# Node ID 0b92f68124e8282fde7cc653db09ad5244e69d00
# Parent  984191be035776640c8a1a1973083865a07080e8
display code theorems with HOL equality

diff -r 984191be0357 -r 0b92f68124e8 doc-src/more_antiquote.ML
--- 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