diff -r f0d9f873f470 -r c742527a25fe src/Tools/Code/code_symbol.ML --- a/src/Tools/Code/code_symbol.ML Thu Aug 01 14:46:50 2019 +0200 +++ b/src/Tools/Code/code_symbol.ML Fri Aug 02 11:23:09 2019 +0200 @@ -99,7 +99,7 @@ local fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy); fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy); - fun thyname_of_instance thy inst = case Axclass.thynames_of_arity thy inst + fun thyname_of_instance thy inst = case Thm.thynames_of_arity thy inst of [] => error ("No such instance: " ^ quote (fst inst ^ " :: " ^ snd inst)) | thyname :: _ => thyname; fun thyname_of_const thy c = case Axclass.class_of_param thy c