# HG changeset patch
# User wenzelm
# Date 1727530911 -7200
# Node ID 8400bba937be94ada47dcc09000927971c232afa
# Parent  2cc651d3ce8ed78de991439c461736575e2a8208
minor performance tuning;

diff -r 2cc651d3ce8e -r 8400bba937be src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Fri Sep 27 23:47:45 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Sat Sep 28 15:41:51 2024 +0200
@@ -540,7 +540,8 @@
     | (Tip t, Tip t') => Lexicon.token_ord (t, t')
     | _ => int_ord (apply2 cons_nr pts));
 
-structure Parsetrees = Table(type key = parsetree list val ord = list_ord parsetree_ord);
+structure Parsetrees =
+  Table(type key = parsetree list val ord = pointer_eq_ord (list_ord parsetree_ord));
 
 end;