# HG changeset patch
# User wenzelm
# Date 1210158313 -7200
# Node ID 612ca951afee318bb7abef3ff072c5320dd7cebd
# Parent  81308d44fe0a380d70ec8173531b28092721d374
output_entity: ignore ThyOutput.source option;

diff -r 81308d44fe0a -r 612ca951afee doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Wed May 07 13:04:12 2008 +0200
+++ b/doc-src/antiquote_setup.ML	Wed May 07 13:05:13 2008 +0200
@@ -140,13 +140,13 @@
 
 val arg = enclose "{" "}" o clean_string;
 
-fun output_entity markup index kind src ctxt (logic, name) =
+fun output_entity markup index kind ctxt (logic, name) =
   (case index of
     NONE => ""
   | SOME is_def =>
       "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name)
   ^
-  (Output.output (if ! O.source then str_of_source src else name)
+  (Output.output name
     |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
     |> (if ! O.quotes then quote else I)
     |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
@@ -154,7 +154,7 @@
 
 fun entity markup index kind =
   O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
-    (output_entity markup index kind);
+    (K (output_entity markup index kind));
     
 fun entity_antiqs markup kind =
  [(kind, entity markup NONE kind),