# HG changeset patch
# User wenzelm
# Date 1526476692 -7200
# Node ID 14dd78f036bad7af49ccaa011ad5890c2faa22db
# Parent  73a1b393d6f90dd537119976e08c0ed0a67ecbce
more thorough checks for theory name consistency (for extend, not just merge);

diff -r 73a1b393d6f9 -r 14dd78f036ba src/Pure/context.ML
--- a/src/Pure/context.ML	Tue May 15 17:07:41 2018 +0200
+++ b/src/Pure/context.ML	Wed May 16 15:18:12 2018 +0200
@@ -359,7 +359,7 @@
 
 val update_thy = change_thy false;
 val extend_thy = update_thy I;
-val finish_thy = change_thy true I;
+val finish_thy = change_thy true I #> tap extend_thy;
 
 end;
 
@@ -399,7 +399,7 @@
 
       val history = make_history name 0;
       val ancestry = make_ancestry parents ancestors;
-    in create_thy ids history ancestry (data_of thy0) end;
+    in create_thy ids history ancestry (data_of thy0) |> tap finish_thy end;
 
 end;