# HG changeset patch
# User wenzelm
# Date 1516357555 -3600
# Node ID 82bc0d5d1ef3dbc53260771ac5e164c86e653934
# Parent  d1697ac0fcd1e895ad7399a82d524a1611b6e710
tuned;

diff -r d1697ac0fcd1 -r 82bc0d5d1ef3 src/Pure/Thy/document_antiquotation.ML
--- a/src/Pure/Thy/document_antiquotation.ML	Fri Jan 19 11:02:13 2018 +0100
+++ b/src/Pure/Thy/document_antiquotation.ML	Fri Jan 19 11:25:55 2018 +0100
@@ -131,7 +131,7 @@
 
 in
 
-val antiq =
+val parse_antiq =
   Parse.!!!
     (Parse.token Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof)
   >> (fn ((name, props), args) => (props, name :: args));
@@ -162,12 +162,14 @@
 
 in
 
-fun evaluate _ (Antiquote.Text ss) = [Latex.symbols ss]
-  | evaluate ctxt (Antiquote.Control {name, body, ...}) =
+fun evaluate ctxt antiq =
+  (case antiq of
+    Antiquote.Text ss => [Latex.symbols ss]
+  | Antiquote.Control {name, body, ...} =>
       eval ctxt ([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
-  | evaluate ctxt (Antiquote.Antiq {range = (pos, _), body, ...}) =
+  | Antiquote.Antiq {range = (pos, _), body, ...} =>
       let val keywords = Thy_Header.get_keywords' ctxt;
-      in eval ctxt (Token.read_antiq keywords antiq (body, pos)) end;
+      in eval ctxt (Token.read_antiq keywords parse_antiq (body, pos)) end);
 
 end;