# HG changeset patch
# User haftmann
# Date 1469371720 -7200
# Node ID d7c6a3a01b79b637926bdf85e5c749356ff43ee1
# Parent  4a72b37ac4b894892903d380a3c1dd1bf9aeef16
simplified

diff -r 4a72b37ac4b8 -r d7c6a3a01b79 src/Doc/more_antiquote.ML
--- a/src/Doc/more_antiquote.ML	Sun Jul 24 16:48:39 2016 +0200
+++ b/src/Doc/more_antiquote.ML	Sun Jul 24 16:48:40 2016 +0200
@@ -25,21 +25,18 @@
 
 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 true [thm] ctxt';
   in thm end;
 
-fun pretty_code_thm ctxt source raw_const =
+fun pretty_code_thm ctxt raw_const =
   let
     val thy = Proof_Context.theory_of ctxt;
     val const = Code.check_const thy raw_const;
@@ -51,13 +48,13 @@
       |> these
       |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
       |> map (holize o no_vars ctxt o Axclass.overload ctxt);
-  in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt source thms) end;
+  in Thy_Output.output ctxt (map (Thy_Output.pretty_thm ctxt) thms) end;
 
 in
 
 val _ =
   Theory.setup (Thy_Output.antiquotation @{binding code_thms} Args.term
-    (fn {source, context, ...} => pretty_code_thm context source));
+    (fn {context, ...} => pretty_code_thm context));
 
 end;