# HG changeset patch
# User haftmann
# Date 1231408428 -3600
# Node ID aab26a65e80f04183056a359c0c862aa94f9cd8e
# Parent  bc41c9cbbfc2b3c935e6ca168c115217cb59e4d7
dded code_thm antiquotation

diff -r bc41c9cbbfc2 -r aab26a65e80f doc-src/more_antiquote.ML
--- a/doc-src/more_antiquote.ML	Thu Jan 08 08:06:11 2009 +0100
+++ b/doc-src/more_antiquote.ML	Thu Jan 08 10:53:48 2009 +0100
@@ -50,7 +50,7 @@
   end
 
 
-(* class antiquotation *)
+(* class and type constructor antiquotation *)
 
 local
 
@@ -74,6 +74,38 @@
 end;
 
 
+(* code theorem antiquotation *)
+
+local
+
+fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
+
+fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
+
+fun no_vars ctxt thm =
+  let
+    val ctxt' = Variable.set_body false ctxt;
+    val ((_, [thm]), _) = Variable.import_thms true [thm] ctxt';
+  in thm end;
+
+fun pretty_code_thm src ctxt raw_const =
+  let
+    val thy = ProofContext.theory_of ctxt;
+    val const = Code_Unit.check_const thy raw_const;
+    val (_, funcgr) = Code_Funcgr.make thy [const];
+    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);
+  in ThyOutput.output_list pretty_thm src ctxt thms end;
+
+in
+
+val _ = O.add_commands
+  [("code_thms", ThyOutput.args Args.term pretty_code_thm)];
+
+end;
+
+
 (* code antiquotation *)
 
 local