src/Pure/theory.ML
changeset 15703 727ef1b8b3ee
parent 15570 8d8c70b41bab
child 15716 1291a8f2ccb1
     1.1 --- a/src/Pure/theory.ML	Wed Apr 13 09:48:41 2005 +0200
     1.2 +++ b/src/Pure/theory.ML	Wed Apr 13 18:34:22 2005 +0200
     1.3 @@ -540,43 +540,32 @@
     1.4  
     1.5  (** merge theories **)          (*exception ERROR*)
     1.6  
     1.7 -fun merge_sign (sg, thy) =
     1.8 -  Sign.nontriv_merge (sg, sign_of thy) handle TERM (msg, _) => error msg;
     1.9 -
    1.10  (*merge list of theories from left to right, preparing extend*)
    1.11  fun prep_ext_merge thys =
    1.12 -  if null thys then
    1.13 -    error "Merge: no parent theories"
    1.14 -  else if exists is_draft thys then
    1.15 -    error "Attempt to merge draft theories"
    1.16 -  else
    1.17 -    let
    1.18 -      val sign' =
    1.19 -        Library.foldl merge_sign (sign_of (hd thys), tl thys)
    1.20 -        |> Sign.prep_ext
    1.21 -        |> Sign.add_path "/";
    1.22 +  let
    1.23 +    val sign' = Sign.prep_ext_merge (map sign_of thys)
    1.24  
    1.25 -      val depss = map (#const_deps o rep_theory) thys;
    1.26 -      val deps' = Library.foldl (Graph.merge_acyclic (K true)) (hd depss, tl depss)
    1.27 -        handle Graph.CYCLES namess => error (cycle_msg namess);
    1.28 +    val depss = map (#const_deps o rep_theory) thys;
    1.29 +    val deps' = Library.foldl (Graph.merge_acyclic (K true)) (hd depss, tl depss)
    1.30 +      handle Graph.CYCLES namess => error (cycle_msg namess);
    1.31 +
    1.32 +    val final_constss = map (#final_consts o rep_theory) thys;
    1.33 +    val final_consts' =
    1.34 +      Library.foldl (Symtab.join (merge_final sign')) (hd final_constss, tl final_constss);
    1.35 +    val axioms' = Symtab.empty;
    1.36  
    1.37 -      val final_constss = map (#final_consts o rep_theory) thys;
    1.38 -      val final_consts' = Library.foldl (Symtab.join (merge_final sign')) (hd final_constss,
    1.39 -								   tl final_constss);
    1.40 -      val axioms' = Symtab.empty;
    1.41 +    fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
    1.42 +    val oracles' =
    1.43 +      Symtab.make (gen_distinct eq_ora
    1.44 +        (List.concat (map (Symtab.dest o #oracles o rep_theory) thys)))
    1.45 +      handle Symtab.DUPS names => err_dup_oras names;
    1.46  
    1.47 -      fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
    1.48 -      val oracles' =
    1.49 -        Symtab.make (gen_distinct eq_ora
    1.50 -          (List.concat (map (Symtab.dest o #oracles o rep_theory) thys)))
    1.51 -        handle Symtab.DUPS names => err_dup_oras names;
    1.52 -
    1.53 -      val parents' = gen_distinct eq_thy thys;
    1.54 -      val ancestors' =
    1.55 -        gen_distinct eq_thy (parents' @ List.concat (map ancestors_of thys));
    1.56 -    in
    1.57 -      make_theory sign' deps' final_consts' axioms' oracles' parents' ancestors'
    1.58 -    end;
    1.59 +    val parents' = gen_distinct eq_thy thys;
    1.60 +    val ancestors' =
    1.61 +      gen_distinct eq_thy (parents' @ List.concat (map ancestors_of thys));
    1.62 +  in
    1.63 +    make_theory sign' deps' final_consts' axioms' oracles' parents' ancestors'
    1.64 +  end;
    1.65  
    1.66  
    1.67  end;