# HG changeset patch
# User blanchet
# Date 1355001344 -3600
# Node ID b233d426fa0bfa531c6f861e76398dd136234ef8
# Parent  4f6a4d32522c76a9cae33c3e4d6cc28966af988b# Parent  955c4aa44f60cc2dac8f0523eee401064fa07527
merge

diff -r 4f6a4d32522c -r b233d426fa0b src/Pure/context.ML
--- a/src/Pure/context.ML	Sat Dec 08 21:54:28 2012 +0100
+++ b/src/Pure/context.ML	Sat Dec 08 22:15:44 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 () =>