src/Pure/PIDE/command.ML
changeset 59058 a78612c67ec0
parent 58934 385a4cc7426f
child 59123 e68e44836d04
--- a/src/Pure/PIDE/command.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/Pure/PIDE/command.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -187,7 +187,7 @@
 datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo};
 
 fun eval_exec_id (Eval {exec_id, ...}) = exec_id;
-val eval_eq = op = o pairself eval_exec_id;
+val eval_eq = op = o apply2 eval_exec_id;
 
 val eval_running = Execution.is_running_exec o eval_exec_id;
 fun eval_finished (Eval {eval_process, ...}) = memo_finished eval_process;
@@ -291,7 +291,7 @@
   exec_id: Document_ID.exec, print_process: unit memo};
 
 fun print_exec_id (Print {exec_id, ...}) = exec_id;
-val print_eq = op = o pairself print_exec_id;
+val print_eq = op = o apply2 print_exec_id;
 
 type print_fn = Toplevel.transition -> Toplevel.state -> unit;