# HG changeset patch
# User wenzelm
# Date 1594991583 -7200
# Node ID deb390860f0790588fc7e2805bba96b3c7659237
# Parent  6c75287276d53edaeefb1bef09f481156f888cc6
clarified -- avoid non-standard extend;

diff -r 6c75287276d5 -r deb390860f07 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Fri Jul 17 15:08:56 2020 +0200
+++ b/src/Pure/global_theory.ML	Fri Jul 17 15:13:03 2020 +0200
@@ -62,7 +62,7 @@
 (
   type T = Facts.T * Thm_Name.T Inttab.table lazy option;
   val empty: T = (Facts.empty, NONE);
-  fun extend (facts, _) = (facts, NONE);
+  val extend = I;
   fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), NONE);
 );