1.1 --- a/src/Pure/context.ML	Sat Dec 08 21:54:28 2012 +0100
     1.2 +++ b/src/Pure/context.ML	Sat Dec 08 22:15:44 2012 +0100
     1.3 @@ -312,17 +312,17 @@
     1.4  
     1.5  (* consistent ancestors *)
     1.6  
     1.7 +fun eq_thy_consistent (thy1, thy2) =
     1.8 +  eq_thy (thy1, thy2) orelse
     1.9 +    (theory_name thy1 = theory_name thy2 andalso
    1.10 +      raise THEORY ("Duplicate theory name", [thy1, thy2]));
    1.11 +
    1.12  fun extend_ancestors thy thys =
    1.13 -  if member eq_thy thys thy then
    1.14 +  if member eq_thy_consistent thys thy then
    1.15      raise THEORY ("Duplicate theory node", thy :: thys)
    1.16    else thy :: thys;
    1.17  
    1.18 -fun extend_ancestors_of thy = extend_ancestors thy (ancestors_of thy);
    1.19 -
    1.20 -val merge_ancestors = merge (fn (thy1, thy2) =>
    1.21 -  eq_thy (thy1, thy2) orelse
    1.22 -    theory_name thy1 = theory_name thy2 andalso
    1.23 -      raise THEORY ("Inconsistent theory versions", [thy1, thy2]));
    1.24 +val merge_ancestors = merge eq_thy_consistent;
    1.25  
    1.26  
    1.27  (* trivial merge *)
    1.28 @@ -361,7 +361,7 @@
    1.29        if draft then (self, data, ancestry)    (*destructive change!*)
    1.30        else if #stage history > 0
    1.31        then (NONE, data, ancestry)
    1.32 -      else (NONE, extend_data data, make_ancestry [thy] (extend_ancestors_of thy));
    1.33 +      else (NONE, extend_data data, make_ancestry [thy] (extend_ancestors thy (ancestors_of thy)));
    1.34      val ids' = insert_id draft id ids;
    1.35      val data'' = f data';
    1.36      val thy' = SYNCHRONIZED (fn () =>