src/Pure/Isar/code_unit.ML
changeset 25597 34860182b250
parent 25540 e209975d5606
child 26112 ac2ce7242eae
     1.1 --- a/src/Pure/Isar/code_unit.ML	Mon Dec 10 11:24:14 2007 +0100
     1.2 +++ b/src/Pure/Isar/code_unit.ML	Mon Dec 10 11:24:15 2007 +0100
     1.3 @@ -60,7 +60,7 @@
     1.4  fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
     1.5  
     1.6  fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy);
     1.7 -fun string_of_const thy c = case Class.inst_of_param thy c
     1.8 +fun string_of_const thy c = case AxClass.inst_of_param thy c
     1.9   of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
    1.10    | NONE => Sign.extern_const thy c;
    1.11  
    1.12 @@ -76,7 +76,7 @@
    1.13      | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
    1.14    end;
    1.15  
    1.16 -fun read_const thy = Class.unoverload_const thy o read_bare_const thy;
    1.17 +fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
    1.18  
    1.19  local
    1.20