src/Pure/sorts.ML
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);