# 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) );