# HG changeset patch
# User haftmann
# Date 1164990153 -3600
# Node ID 17098171d46aefc6f1c2cf19c2c2c5c8ce99aa34
# Parent  5825a59785f4d3d2e0c9fc9a4747340a3e70e6aa
non-exported syntax

diff -r 5825a59785f4 -r 17098171d46a src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Fri Dec 01 17:22:32 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Fri Dec 01 17:22:33 2006 +0100
@@ -322,6 +322,10 @@
     val mapp_sup = AList.make
       (the o AList.lookup (op =) ((flat o map (the_parm_map thy) o the_ancestry thy) supclasses))
       ((map (fst o fst) o Locale.parameters_of_expr thy) expr_supclasses);
+    fun unlocalize syn =
+      let
+        val syn' = Syntax.unlocalize_mixfix true syn;
+      in if syn = syn' then NoSyn else syn' end;
     fun extract_tyvar_consts thy name_locale =
       let
         fun extract_classvar ((c, ty), _) w =
@@ -333,7 +337,7 @@
             | _ => error ("More than one type variable in type signature of constant " ^ quote c));
         val consts1 =
           Locale.parameters_of thy name_locale
-          |> map (apsnd (Syntax.unlocalize_mixfix true))
+          |> map (apsnd unlocalize)
         val SOME v = fold extract_classvar consts1 NONE;
         val consts2 = map ((apfst o apsnd) (subst_clsvar v (TFree (v, [])))) consts1;
       in (v, chop (length mapp_sup) consts2) end;