--- a/src/Pure/Isar/code_unit.ML Mon Dec 10 11:24:14 2007 +0100
+++ b/src/Pure/Isar/code_unit.ML Mon Dec 10 11:24:15 2007 +0100
@@ -60,7 +60,7 @@
fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy);
-fun string_of_const thy c = case Class.inst_of_param thy c
+fun string_of_const thy c = case AxClass.inst_of_param thy c
of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
| NONE => Sign.extern_const thy c;
@@ -76,7 +76,7 @@
| NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
end;
-fun read_const thy = Class.unoverload_const thy o read_bare_const thy;
+fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
local