# HG changeset patch
# User wenzelm
# Date 1667505201 -3600
# Node ID 2b0ff7c52aa4c540f036e3c90ff45232484a68c0
# Parent  e937d14b58e287a3257fb11a20290afbd34dafde
tuned;

diff -r e937d14b58e2 -r 2b0ff7c52aa4 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu Nov 03 20:42:27 2022 +0100
+++ b/src/Pure/PIDE/command.ML	Thu Nov 03 20:53:21 2022 +0100
@@ -309,6 +309,7 @@
 
 fun print_exec_id (Print {exec_id, ...}) = exec_id;
 val print_eq = op = o apply2 print_exec_id;
+fun print_equiv (name', args') (Print {name, args, ...}) = name' = name andalso args' = args;
 
 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
 
@@ -380,7 +381,7 @@
       end;
 
     fun get_print (name, args) =
-      (case find_first (fn Print print => (#name print, #args print) = (name, args)) old_prints of
+      (case find_first (print_equiv (name, args)) old_prints of
         NONE =>
           (case AList.lookup (op =) print_functions name of
             NONE =>