tuned;
authorwenzelm
Thu, 03 Nov 2022 20:53:21 +0100
changeset 76418 2b0ff7c52aa4
parent 76417 e937d14b58e2
child 76419 f20865ad6319
tuned;
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 =>