# HG changeset patch
# User wenzelm
# Date 1703872817 -3600
# Node ID b9d80d5aca8ed835bfc8d0475cd76f138e8ecedc
# Parent  e31b48b47e88baa094b9b129a512a3bcee948bc9
more operations;

diff -r e31b48b47e88 -r b9d80d5aca8e src/Pure/term_items.ML
--- a/src/Pure/term_items.ML	Fri Dec 29 15:58:43 2023 +0100
+++ b/src/Pure/term_items.ML	Fri Dec 29 19:00:17 2023 +0100
@@ -220,3 +220,6 @@
 val add_free_names = fold_aterms (fn Free (x, _) => add_set x | _ => I);
 
 end;
+
+
+structure Types = Term_Items(type key = typ val ord = Term_Ord.typ_ord);