src/Pure/Isar/code.ML
changeset 42359 6ca5407863ed
parent 41493 f05976d69141
child 42360 da8817d01e7c
     1.1 --- a/src/Pure/Isar/code.ML	Sat Apr 16 13:48:45 2011 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Sat Apr 16 15:25:25 2011 +0200
     1.3 @@ -112,9 +112,14 @@
     1.4  fun string_of_typ thy =
     1.5    Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy));
     1.6  
     1.7 -fun string_of_const thy c = case AxClass.inst_of_param thy c
     1.8 - of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
     1.9 -  | NONE => Sign.extern_const thy c;
    1.10 +fun string_of_const thy c =
    1.11 +  let val ctxt = ProofContext.init_global thy in
    1.12 +    case AxClass.inst_of_param thy c of
    1.13 +      SOME (c, tyco) =>
    1.14 +        ProofContext.extern_const ctxt c ^ " " ^ enclose "[" "]"
    1.15 +          (ProofContext.extern_type ctxt tyco)
    1.16 +    | NONE => ProofContext.extern_const ctxt c
    1.17 +  end;
    1.18  
    1.19  
    1.20  (* constants *)