src/Pure/cterm_items.ML
changeset 79121 6a84d18fa548
parent 77903 38d0a90e87c1
child 79162 c1bbaa0d89b4
--- a/src/Pure/cterm_items.ML	Mon Dec 04 12:10:39 2023 +0100
+++ b/src/Pure/cterm_items.ML	Mon Dec 04 19:24:39 2023 +0100
@@ -33,7 +33,7 @@
 structure Term_Items = Term_Items
 (
   type key = cterm;
-  val ord = Thm.fast_term_ord
+  val ord = Thm.fast_term_ord;
 );
 open Term_Items;