merge/merge_refs: plain error instead of exception TERM;
authorwenzelm
Wed Jun 13 00:01:58 2007 +0200 (2007-06-13)
changeset 23355d2c033fd4514
parent 23354 a189707c1d76
child 23356 dbe3731241c3
merge/merge_refs: plain error instead of exception TERM;
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Wed Jun 13 00:01:57 2007 +0200
     1.2 +++ b/src/Pure/context.ML	Wed Jun 13 00:01:58 2007 +0200
     1.3 @@ -38,8 +38,8 @@
     1.4    val thy_ord: theory * theory -> order
     1.5    val subthy: theory * theory -> bool
     1.6    val joinable: theory * theory -> bool
     1.7 -  val merge: theory * theory -> theory                     (*exception TERM*)
     1.8 -  val merge_refs: theory_ref * theory_ref -> theory_ref    (*exception TERM*)
     1.9 +  val merge: theory * theory -> theory
    1.10 +  val merge_refs: theory_ref * theory_ref -> theory_ref
    1.11    val self_ref: theory -> theory_ref
    1.12    val deref: theory_ref -> theory
    1.13    val copy_thy: theory -> theory
    1.14 @@ -227,17 +227,16 @@
    1.15  val str_of_thy = Pretty.str_of o pretty_abbrev_thy;
    1.16  
    1.17  
    1.18 -(* consistency *)    (*exception TERM*)
    1.19 +(* consistency *)
    1.20  
    1.21  fun check_thy thy =
    1.22 -  if is_stale thy then
    1.23 -    raise TERM ("Stale theory encountered:\n" ^ string_of_thy thy, [])
    1.24 +  if is_stale thy then error ("Stale theory encountered:\n" ^ string_of_thy thy)
    1.25    else thy;
    1.26  
    1.27  fun check_ins id ids =
    1.28    if draft_id id orelse Inttab.defined ids (#1 id) then ids
    1.29    else if Inttab.exists (equal (#2 id) o #2) ids then
    1.30 -    raise TERM ("Different versions of theory component " ^ quote (#2 id), [])
    1.31 +    error ("Different versions of theory component " ^ quote (#2 id))
    1.32    else Inttab.update id ids;
    1.33  
    1.34  fun check_insert intermediate id (ids, iids) =
    1.35 @@ -278,15 +277,15 @@
    1.36  fun deref (TheoryRef (ref thy)) = thy;
    1.37  
    1.38  
    1.39 -(* trivial merge *)    (*exception TERM*)
    1.40 +(* trivial merge *)
    1.41  
    1.42  fun merge (thy1, thy2) =
    1.43    if eq_thy (thy1, thy2) then thy1
    1.44    else if proper_subthy (thy2, thy1) then thy1
    1.45    else if proper_subthy (thy1, thy2) then thy2
    1.46    else (check_merge thy1 thy2;
    1.47 -    raise TERM (cat_lines ["Attempt to perform non-trivial merge of theories:",
    1.48 -      str_of_thy thy1, str_of_thy thy2], []));
    1.49 +    error (cat_lines ["Attempt to perform non-trivial merge of theories:",
    1.50 +      str_of_thy thy1, str_of_thy thy2]));
    1.51  
    1.52  fun merge_refs (ref1, ref2) =
    1.53    if ref1 = ref2 then ref1