# HG changeset patch
# User wenzelm
# Date 1287519190 -3600
# Node ID b70cd46e8e4488747e56cfe6c5ed7fdde108560d
# Parent  2b88d00d67901c55d5f616f4646c5112be30e33a
more robust treatment of "op IDENT";

diff -r 2b88d00d6790 -r b70cd46e8e44 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Tue Oct 19 21:01:34 2010 +0100
+++ b/doc-src/antiquote_setup.ML	Tue Oct 19 21:13:10 2010 +0100
@@ -71,7 +71,7 @@
         if txt2 = "" then txt1
         else if kind = "type" then txt1 ^ " = " ^ txt2
         else if kind = "exception" then txt1 ^ " of " ^ txt2
-        else if Syntax.is_identifier (Long_Name.base_name txt1) then txt1 ^ ": " ^ txt2
+        else if Syntax.is_identifier (Long_Name.base_name (ml_name txt1)) then txt1 ^ ": " ^ txt2
         else txt1 ^ " : " ^ txt2;
       val txt' = if kind = "" then txt else kind ^ " " ^ txt;
       val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none (ml (txt1, txt2));  (* ML_Lex.read (!?) *)