diff -r 9bea6244c35a -r 0e4d8aa61ad7 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sat Nov 20 19:39:22 2021 +0100
+++ b/src/Pure/Thy/latex.ML	Sat Nov 20 20:42:41 2021 +0100
@@ -22,10 +22,6 @@
   val output_syms: string -> string
   val symbols: Symbol_Pos.T list -> text
   val symbols_output: Symbol_Pos.T list -> text
-  val begin_delim: string -> string
-  val end_delim: string -> string
-  val begin_tag: string -> string
-  val end_tag: string -> string
   val environment_text: string -> text -> text
   val isabelle_body: string -> text -> text
   val theory_entry: string -> string
@@ -196,14 +192,6 @@
   text (output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms));
 
 
-(* tags *)
-
-val begin_delim = enclose_name "%\n\\isadelim" "\n";
-val end_delim = enclose_name "%\n\\endisadelim" "\n";
-val begin_tag = enclose_name "%\n\\isatag" "\n";
-fun end_tag tg = enclose_name "%\n\\endisatag" "\n" tg ^ enclose_name "{\\isafold" "}%\n" tg;
-
-
 (* theory presentation *)
 
 fun environment_text name =