diff -r 702278df3b57 -r 955c4aa44f60 src/Pure/context.ML
--- a/src/Pure/context.ML	Fri Dec 07 23:14:39 2012 +0100
+++ b/src/Pure/context.ML	Sat Dec 08 13:25:49 2012 +0100
@@ -312,17 +312,17 @@
 
 (* consistent ancestors *)
 
+fun eq_thy_consistent (thy1, thy2) =
+  eq_thy (thy1, thy2) orelse
+    (theory_name thy1 = theory_name thy2 andalso
+      raise THEORY ("Duplicate theory name", [thy1, thy2]));
+
 fun extend_ancestors thy thys =
-  if member eq_thy thys thy then
+  if member eq_thy_consistent thys thy then
     raise THEORY ("Duplicate theory node", thy :: thys)
   else thy :: thys;
 
-fun extend_ancestors_of thy = extend_ancestors thy (ancestors_of thy);
-
-val merge_ancestors = merge (fn (thy1, thy2) =>
-  eq_thy (thy1, thy2) orelse
-    theory_name thy1 = theory_name thy2 andalso
-      raise THEORY ("Inconsistent theory versions", [thy1, thy2]));
+val merge_ancestors = merge eq_thy_consistent;
 
 
 (* trivial merge *)
@@ -361,7 +361,7 @@
       if draft then (self, data, ancestry)    (*destructive change!*)
       else if #stage history > 0
       then (NONE, data, ancestry)
-      else (NONE, extend_data data, make_ancestry [thy] (extend_ancestors_of thy));
+      else (NONE, extend_data data, make_ancestry [thy] (extend_ancestors thy (ancestors_of thy)));
     val ids' = insert_id draft id ids;
     val data'' = f data';
     val thy' = SYNCHRONIZED (fn () =>