diff -r 26b80ed2259b -r ba72eac54f05 src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Sat Jan 28 17:29:03 2006 +0100 +++ b/src/Pure/Tools/class_package.ML Sat Jan 28 17:29:04 2006 +0100 @@ -192,8 +192,7 @@ (fn (Element.Fixes consts) => SOME consts | _ => NONE) |> Library.flat - |> map (fn (c, ty, syn) => - ((c, the ty), (Syntax.unlocalize_mixfix o Syntax.fix_mixfix c) syn)) + |> map (fn (c, ty, syn) => ((c, the ty), Syntax.unlocalize_mixfix syn)) val import_consts = get_elems import_elems; val body_consts = get_elems body_elems; val v = extract_tyvar_name thy (map (snd o fst) (import_consts @ body_consts));