1.1 --- a/doc-src/antiquote_setup.ML	Wed May 07 13:04:12 2008 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Wed May 07 13:05:13 2008 +0200
     1.3 @@ -140,13 +140,13 @@
     1.4  
     1.5  val arg = enclose "{" "}" o clean_string;
     1.6  
     1.7 -fun output_entity markup index kind src ctxt (logic, name) =
     1.8 +fun output_entity markup index kind ctxt (logic, name) =
     1.9    (case index of
    1.10      NONE => ""
    1.11    | SOME is_def =>
    1.12        "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name)
    1.13    ^
    1.14 -  (Output.output (if ! O.source then str_of_source src else name)
    1.15 +  (Output.output name
    1.16      |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
    1.17      |> (if ! O.quotes then quote else I)
    1.18      |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.19 @@ -154,7 +154,7 @@
    1.20  
    1.21  fun entity markup index kind =
    1.22    O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
    1.23 -    (output_entity markup index kind);
    1.24 +    (K (output_entity markup index kind));
    1.25      
    1.26  fun entity_antiqs markup kind =
    1.27   [(kind, entity markup NONE kind),