# HG changeset patch # User haftmann # Date 1214467611 -7200 # Node ID 91a7041a5a6416e7fe8df2ca7aec112255f1f580 # Parent a8672b0e2b156a08a0314c4cc987382092adef43 class theory name lookup improved diff -r a8672b0e2b15 -r 91a7041a5a64 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));