1.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Apr 08 14:05:31 2011 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Apr 08 14:20:57 2011 +0200
     1.3 @@ -178,7 +178,7 @@
     1.4  
     1.5  (* Compatibility. *)
     1.6  
     1.7 -val string_of_mixfix = Pretty.string_of o Syntax.pretty_mixfix;
     1.8 +val string_of_mixfix = Pretty.string_of o Mixfix.pretty_mixfix;
     1.9  
    1.10  fun mk_syn thy c =
    1.11    if Syntax.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn