# HG changeset patch
# User wenzelm
# Date 1114278605 -7200
# Node ID e9b4c9feb296141fbd19b39a87c043fd59c87dfb
# Parent  1576f9d3ffae5196d57f0866557f1a60980aeee9
improved read_tyname;
merge_stamps, merge_refs: error instead of raise TERM;

diff -r 1576f9d3ffae -r e9b4c9feb296 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sat Apr 23 19:49:49 2005 +0200
+++ b/src/Pure/sign.ML	Sat Apr 23 19:50:05 2005 +0200
@@ -777,7 +777,7 @@
   let val c = intern_tycon sg raw_c in
     (case Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c) of
       SOME (Type.LogicalType n, _) => Type (c, replicate n dummyT)
-    | NONE => raise TYPE ("Undeclared type constructor: " ^ quote c, [], []))
+    | _ => raise TYPE ("Undeclared type constructor: " ^ quote c, [], []))
   end;
 
 fun read_const sg raw_c =
@@ -1163,8 +1163,7 @@
   let val stamps = merge_lists' stamps1 stamps2 in
     (case duplicates (map ! stamps) of
       [] => stamps
-    | dups => raise TERM ("Attempt to merge different versions of theories "
-        ^ commas_quote dups, []))
+    | dups => error ("Attempt to merge different versions of theories " ^ commas_quote dups))
   end;
 
 
@@ -1175,7 +1174,7 @@
       if subsig (sg2, sg1) then sgr1
       else if subsig (sg1, sg2) then sgr2
       else (merge_stamps s1 s2; (*check for different versions*)
-        raise TERM ("Attempt to do non-trivial merge of signatures", []))
+        error "Attempt to do non-trivial merge of signatures")
   | merge_refs _ = sys_error "Sign.merge_refs";
 
 val merge = deref o merge_refs o pairself self_ref;