# HG changeset patch
# User wenzelm
# Date 1630691763 -7200
# Node ID bf595bfbdc98f38961adb12f6696ef7b26090340
# Parent  291e71ed0174295baae58d3296f60cf5f8a930f1
tuned;

diff -r 291e71ed0174 -r bf595bfbdc98 src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Fri Sep 03 19:55:57 2021 +0200
+++ b/src/Pure/term_subst.ML	Fri Sep 03 19:56:03 2021 +0200
@@ -59,22 +59,22 @@
 
 structure TFrees = Inst_Table(
   type key = string * sort
-  val ord = prod_ord fast_string_ord Term_Ord.sort_ord
+  val ord = pointer_eq_ord (prod_ord fast_string_ord Term_Ord.sort_ord)
 );
 
 structure TVars = Inst_Table(
   type key = indexname * sort
-  val ord = prod_ord Term_Ord.fast_indexname_ord Term_Ord.sort_ord
+  val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.sort_ord)
 );
 
 structure Frees = Inst_Table(
   type key = string * typ
-  val ord = prod_ord fast_string_ord Term_Ord.typ_ord
+  val ord = pointer_eq_ord (prod_ord fast_string_ord Term_Ord.typ_ord)
 );
 
 structure Vars = Inst_Table(
   type key = indexname * typ
-  val ord = prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord
+  val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord)
 );