# HG changeset patch
# User wenzelm
# Date 1681895430 -7200
# Node ID 41f1fd0fdb80a62158f6c00d9dd5bef96508f94c
# Parent  dd222e2af01a2e4e817d8406e4a6d9c669593615
tuned;

diff -r dd222e2af01a -r 41f1fd0fdb80 src/Pure/context.ML
--- a/src/Pure/context.ML	Tue Apr 18 22:24:48 2023 +0200
+++ b/src/Pure/context.ML	Wed Apr 19 11:10:30 2023 +0200
@@ -363,7 +363,7 @@
 in
 
 val update_thy = change_thy false;
-val extend_thy = update_thy I;
+val extend_thy = change_thy false I;
 val finish_thy = change_thy true I;
 
 end;