removed unnecessary Syntax.fix_mixfix;
authorwenzelm
Sat, 28 Jan 2006 17:29:04 +0100
changeset 18829 ba72eac54f05
parent 18828 26b80ed2259b
child 18830 34b51dcdc570
removed unnecessary Syntax.fix_mixfix;
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));