equal
deleted
inserted
replaced
97 end; |
97 end; |
98 |
98 |
99 local |
99 local |
100 fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy); |
100 fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy); |
101 fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy); |
101 fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy); |
102 fun thyname_of_instance thy inst = case Axclass.thynames_of_arity thy inst |
102 fun thyname_of_instance thy inst = case Thm.thynames_of_arity thy inst |
103 of [] => error ("No such instance: " ^ quote (fst inst ^ " :: " ^ snd inst)) |
103 of [] => error ("No such instance: " ^ quote (fst inst ^ " :: " ^ snd inst)) |
104 | thyname :: _ => thyname; |
104 | thyname :: _ => thyname; |
105 fun thyname_of_const thy c = case Axclass.class_of_param thy c |
105 fun thyname_of_const thy c = case Axclass.class_of_param thy c |
106 of SOME class => thyname_of_class thy class |
106 of SOME class => thyname_of_class thy class |
107 | NONE => (case Code.get_type_of_constr_or_abstr thy c |
107 | NONE => (case Code.get_type_of_constr_or_abstr thy c |