changeset 43792 | d5803c3d537a |
parent 42387 | b1965c8992c8 |
child 44338 | 700008399ee5 |
--- a/src/Pure/sorts.ML Wed Jul 13 10:57:09 2011 +0200 +++ b/src/Pure/sorts.ML Wed Jul 13 16:42:14 2011 +0200 @@ -185,8 +185,8 @@ (* certify *) fun certify_class algebra c = - if can (Graph.get_node (classes_of algebra)) c then c - else raise TYPE ("Undeclared class: " ^ quote c, [], []); + #1 (Graph.get_entry (classes_of algebra) c) + handle Graph.UNDEF _ => raise TYPE ("Undeclared class: " ^ quote c, [], []); fun certify_sort classes = map (certify_class classes);