diff -r 45ab32a542fe -r dd8ec9138112 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Sun Nov 30 13:15:04 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Sun Nov 30 14:02:48 2014 +0100
@@ -37,28 +37,29 @@
 
 local
 
-val ml_toks = ML_Lex.read Position.none;
+fun ml_val (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read ");"
+  | ml_val (toks1, toks2) =
+      ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");";
 
-fun ml_val (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks ");"
-  | ml_val (toks1, toks2) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks ");";
-
-fun ml_op (toks1, []) = ml_toks "fn _ => (op " @ toks1 @ ml_toks ");"
-  | ml_op (toks1, toks2) = ml_toks "fn _ => (op " @ toks1 @ ml_toks " : " @ toks2 @ ml_toks ");";
+fun ml_op (toks1, []) = ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read ");"
+  | ml_op (toks1, toks2) =
+      ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");";
 
-fun ml_type (toks1, []) = ml_toks "val _ = NONE : (" @ toks1 @ ml_toks ") option;"
+fun ml_type (toks1, []) = ML_Lex.read "val _ = NONE : (" @ toks1 @ ML_Lex.read ") option;"
   | ml_type (toks1, toks2) =
-      ml_toks "val _ = [NONE : (" @ toks1 @ ml_toks ") option, NONE : (" @
-        toks2 @ ml_toks ") option];";
+      ML_Lex.read "val _ = [NONE : (" @ toks1 @ ML_Lex.read ") option, NONE : (" @
+        toks2 @ ML_Lex.read ") option];";
 
-fun ml_exception (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : exn);"
+fun ml_exception (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : exn);"
   | ml_exception (toks1, toks2) =
-      ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks " -> exn);";
+      ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read " -> exn);";
 
 fun ml_structure (toks, _) =
-  ml_toks "functor XXX() = struct structure XX = " @ toks @ ml_toks " end;";
+  ML_Lex.read "functor XXX() = struct structure XX = " @ toks @ ML_Lex.read " end;";
 
 fun ml_functor (Antiquote.Text tok :: _, _) =
-      ml_toks "ML_Env.check_functor " @ ml_toks (ML_Syntax.print_string (ML_Lex.content_of tok))
+      ML_Lex.read "ML_Env.check_functor " @
+      ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok))
   | ml_functor _ = raise Fail "Bad ML functor specification";
 
 val is_name = ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.LongIdent);