src/Pure/context.ML
changeset 26957 e3f04fdd994d
parent 26889 ccea41fb5c39
child 27341 97e2ccba3b64
     1.1 --- a/src/Pure/context.ML	Sun May 18 17:03:16 2008 +0200
     1.2 +++ b/src/Pure/context.ML	Sun May 18 17:03:20 2008 +0200
     1.3 @@ -23,7 +23,6 @@
     1.4    val ancestors_of: theory -> theory list
     1.5    val is_stale: theory -> bool
     1.6    val PureN: string
     1.7 -  val CPureN: string
     1.8    val is_draft: theory -> bool
     1.9    val exists_name: string -> theory -> bool
    1.10    val names_of: theory -> string list
    1.11 @@ -197,7 +196,6 @@
    1.12  (* names *)
    1.13  
    1.14  val PureN = "Pure";
    1.15 -val CPureN = "CPure";
    1.16  
    1.17  val draftN = "#";
    1.18  fun draft_id (_, name) = (name = draftN);
    1.19 @@ -340,18 +338,15 @@
    1.20  (* named theory nodes *)
    1.21  
    1.22  fun merge_thys pp (thy1, thy2) =
    1.23 -  if exists_name CPureN thy1 <> exists_name CPureN thy2 then
    1.24 -    error "Cannot merge Pure and CPure developments"
    1.25 -  else
    1.26 -    let
    1.27 -      val (ids, iids) = check_merge thy1 thy2;
    1.28 -      val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
    1.29 -      val ancestry = make_ancestry [] [];
    1.30 -      val history = make_history "" 0 [];
    1.31 -      val thy' = NAMED_CRITICAL "theory" (fn () =>
    1.32 -       (check_thy thy1; check_thy thy2;
    1.33 -        create_thy draftN NONE (serial (), draftN) ids iids data ancestry history))
    1.34 -    in thy' end;
    1.35 +  let
    1.36 +    val (ids, iids) = check_merge thy1 thy2;
    1.37 +    val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
    1.38 +    val ancestry = make_ancestry [] [];
    1.39 +    val history = make_history "" 0 [];
    1.40 +    val thy' = NAMED_CRITICAL "theory" (fn () =>
    1.41 +     (check_thy thy1; check_thy thy2;
    1.42 +      create_thy draftN NONE (serial (), draftN) ids iids data ancestry history))
    1.43 +  in thy' end;
    1.44  
    1.45  fun maximal_thys thys =
    1.46    thys |> filter (fn thy => not (exists (fn thy' => proper_subthy (thy, thy')) thys));