--- 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 =