src/Pure/Thy/latex.ML

--- a/src/Pure/Thy/latex.ML	Fri Aug 23 15:04:00 2013 +0200
+++ b/src/Pure/Thy/latex.ML	Fri Aug 23 15:36:54 2013 +0200
@@ -99,9 +99,7 @@
   (fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss)
     | Antiquote.Antiq (ss, _) =>
         enclose "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n"
-          (output_symbols (map Symbol_Pos.symbol ss))
-    | Antiquote.Open _ => "{\\isaantiqopen}"
-    | Antiquote.Close _ => "{\\isaantiqclose}");
+          (output_symbols (map Symbol_Pos.symbol ss)));
 
 end;