class theory name lookup improved
authorhaftmann
Thu, 26 Jun 2008 10:06:51 +0200
changeset 27365 91a7041a5a64
parent 27364 a8672b0e2b15
child 27366 d0cda1ea705e
class theory name lookup improved
src/Tools/code/code_name.ML
--- a/src/Tools/code/code_name.ML	Wed Jun 25 22:11:17 2008 +0200
+++ b/src/Tools/code/code_name.ML	Thu Jun 26 10:06:51 2008 +0200
@@ -179,9 +179,7 @@
    of SOME thy => Context.theory_name thy
     | NONE => error (errmsg x) end;
 
-fun thyname_of_class thy =
-  thyname_of' thy (fn thy => member (op =) (Sign.all_classes thy))
-    (fn class => "thyname_of_class: no such class: " ^ quote class);
+fun thyname_of_class thy = thyname_of thy (ProofContext.query_class (ProofContext.init thy));
 
 fun thyname_of_tyco thy = thyname_of thy (Type.the_tags (Sign.tsig_of thy));