more thorough checks for theory name consistency (for extend, not just merge);

--- 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;