# HG changeset patch
# User wenzelm
# Date 1667072193 -7200
# Node ID f227ff7bff500b9f19a7bf3251ce1a2184cd42dc
# Parent  3fa81de0b6c55fd94f64d6aeb569fb78c882adad
tuned signature;

diff -r 3fa81de0b6c5 -r f227ff7bff50 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Oct 28 16:25:44 2022 +0200
+++ b/src/Pure/PIDE/markup.ML	Sat Oct 29 21:36:33 2022 +0200
@@ -250,7 +250,6 @@
   val session_timing: Properties.entry
   val loading_theory: string -> Properties.T
   val build_session_finished: Properties.T
-  val print_operationsN: string
   val print_operations: Properties.T
   val exportN: string
   type export_args =
@@ -773,12 +772,11 @@
 
 val session_timing = (functionN, "session_timing");
 
-fun loading_theory name = [("function", "loading_theory"), (nameN, name)];
+fun loading_theory name = [(functionN, "loading_theory"), (nameN, name)];
 
-val build_session_finished = [("function", "build_session_finished")];
+val build_session_finished = [(functionN, "build_session_finished")];
 
-val print_operationsN = "print_operations";
-val print_operations = [(functionN, print_operationsN)];
+val print_operations = [(functionN, "print_operations")];
 
 
 (* export *)