merged

--- a/doc-src/more_antiquote.ML	Wed Jan 07 23:56:56 2009 +0100
+++ b/doc-src/more_antiquote.ML	Thu Jan 08 12:15:23 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

--- a/src/Pure/Isar/proof.ML	Wed Jan 07 23:56:56 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Jan 08 12:15:23 2009 +0100
@@ -345,7 +345,7 @@
       (case filter_out (fn s => s = "") strs of [] => ""
       | strs' => enclose " (" ")" (commas strs'));
 
-    fun prt_goal (SOME (ctxt, (i, {statement = ((_, pos), _, _), messages, using, goal, ...}))) =
+    fun prt_goal (SOME (ctxt, (i, {statement = ((_, pos), _, _), messages, using, goal, before_qed, after_qed}))) =
           pretty_facts "using " ctxt
             (if mode <> Backward orelse null using then NONE else SOME using) @
           [Pretty.str ("goal" ^