more robust treatment of "op IDENT";
authorwenzelm
Tue, 19 Oct 2010 21:13:10 +0100
changeset 39873 b70cd46e8e44
parent 39872 2b88d00d6790
child 39874 bbac63bbcffe
more robust treatment of "op IDENT";
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 (!?) *)